Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/BNF/Tools/bnf_comp.ML
changeset 51758 55963309557b
parent 51757 7babcb61aa5c
child 51761 4c9f08836d87 
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 13:16:20 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Wed Apr 24 13:16:21 2013 +0200
@@ -261,8 +261,8 @@
         (maps wit_thms_of_bnf inners);
 
     val (bnf', lthy') =
-      bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) []
-        (((((b, mapx), sets), bd), wits), SOME rel) lthy;
+      bnf_def const_policy (K Dont_Note) qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty
+        [] (((((b, mapx), sets), bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   end;
@@ -359,8 +359,8 @@
     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
 
     val (bnf', lthy') =
-      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) []
-        (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
+      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME (killedAs @ Ds)) Binding.empty
+        [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   end;
@@ -443,7 +443,7 @@
     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
 
     val (bnf', lthy') =
-      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) []
+      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty []
         (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
 
   in
@@ -520,7 +520,7 @@
     fun wit_tac _ = mk_simple_wit_tac (wit_thms_of_bnf bnf);
 
     val (bnf', lthy') =
-      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) []
+      bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty []
         (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
@@ -662,7 +662,8 @@
 
     fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
 
-    val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) I tacs wit_tac (SOME deads) []
+    val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) I tacs wit_tac (SOME deads)
+      Binding.empty []
       (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
   in
     ((bnf', deads), lthy')
isabelle