merged

Fri, 09 Aug 2019 17:45:42 +0200

author
wenzelm
date
Fri, 09 Aug 2019 17:45:42 +0200
changeset 10542
81693892c467
parent 10540
108bd2e832e7 (current diff)
parent 10541
e9c5689b8015 (diff)
child 10543
10112f5276d1

merged

--- a/thys/Dict_Construction/side_conditions.ML	Fri Aug 09 15:36:14 2019 +0200
+++ b/thys/Dict_Construction/side_conditions.ML	Fri Aug 09 17:45:42 2019 +0200
@@ -212,7 +212,7 @@
 
     val alts =
       try (Goal.prove_common lthy' NONE frees [] props) tactic
-      |> Option.map (map (mk_eq o Thm.close_derivation))
+      |> Option.map (map (mk_eq o Thm.close_derivation \<^here>))
 
     val _ =
       if is_none alts then
--- a/thys/Nominal2/nominal_function.ML	Fri Aug 09 15:36:14 2019 +0200
+++ b/thys/Nominal2/nominal_function.ML	Fri Aug 09 17:45:42 2019 +0200
@@ -146,7 +146,7 @@
       let
         val NominalFunctionResult {fs, R, psimps, simple_pinducts,
           termination, domintros, cases, eqvts, ...} =
-          cont lthy (Thm.close_derivation proof)
+          cont lthy (Thm.close_derivation \<^here> proof)
 
         val fnames = map (fst o fst) fixes
         fun qualify n = Binding.name n
--- a/thys/Nominal2/nominal_function_core.ML	Fri Aug 09 15:36:14 2019 +0200
+++ b/thys/Nominal2/nominal_function_core.ML	Fri Aug 09 17:45:42 2019 +0200
@@ -355,7 +355,7 @@
       |> fold_rev (Thm.implies_intr o Thm.cprop_of) h_assums
       |> fold_rev (Thm.implies_intr o Thm.cprop_of) ags
       |> fold_rev Thm.forall_intr cqs
-      |> Thm.close_derivation
+      |> Thm.close_derivation \<^here>
   in
     replace_lemma
   end
@@ -382,7 +382,7 @@
     |> map (fold_rev (Thm.implies_intr o Thm.cprop_of) ags)
     |> map (Thm.implies_intr (Thm.cprop_of case_hyp))
     |> map (fold_rev Thm.forall_intr cqs)
-    |> map (Thm.close_derivation)
+    |> map (Thm.close_derivation \<^here>)
   end
 
 (* nominal *)
@@ -406,7 +406,7 @@
     |> map (fold_rev (Thm.implies_intr o Thm.cprop_of) ags)
     |> map (Thm.implies_intr (Thm.cprop_of case_hyp))
     |> map (fold_rev Thm.forall_intr cqs)
-    |> map (Thm.close_derivation)
+    |> map (Thm.close_derivation \<^here>)
   end
 
 (* nominal *)
@@ -587,7 +587,7 @@
 
     val goalstate =
       Conjunction.intr (Conjunction.intr (Conjunction.intr graph_is_function complete) invariant) G_eqvt
-      |> Thm.close_derivation
+      |> Thm.close_derivation \<^here>
       |> Goal.protect 0
       |> fold_rev (Thm.implies_intr o Thm.cprop_of) compat
       |> Thm.implies_intr (Thm.cprop_of complete)
--- a/thys/Nominal2/nominal_termination.ML	Fri Aug 09 15:36:14 2019 +0200
+++ b/thys/Nominal2/nominal_termination.ML	Fri Aug 09 17:45:42 2019 +0200
@@ -46,7 +46,7 @@
                    (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
       fun afterqed [[totality]] lthy =
         let
-          val totality = Thm.close_derivation totality
+          val totality = Thm.close_derivation \<^here> totality
           val remove_domain_condition =
             full_simplify (put_simpset HOL_basic_ss lthy
               addsimps [totality, @{thm True_implies_equals}])

mercurial