# HG changeset patch
# User wenzelm
# Date 1466584853 -7200
# Node ID c9910404cc8addc4c5d8003efb3535d2237e9702
# Parent  fb5d8a50c641d50443207688ae89286f7fdcccf4
tuned signature;
tuned;

diff -r fb5d8a50c641 -r c9910404cc8a src/HOL/Library/simps_case_conv.ML
--- a/src/HOL/Library/simps_case_conv.ML	Wed Jun 22 10:09:20 2016 +0200
+++ b/src/HOL/Library/simps_case_conv.ML	Wed Jun 22 10:40:53 2016 +0200
@@ -136,8 +136,8 @@
       let
         val frees = fold Term.add_frees pat []
         val abs_rhs = fold absfree frees rhs
-        val ((f,def), lthy') = Local_Defs.add_def
-          ((Binding.name name, Mixfix.NoSyn), abs_rhs) lthy
+        val ([(f, (_, def))], lthy') = lthy
+          |> Local_Defs.define [((Binding.name name, Mixfix.NoSyn), (Thm.empty_binding, abs_rhs))]
       in ((list_comb (f, map Free (rev frees)), def), lthy') end
 
     val ((def_ts, def_thms), ctxt2) =
diff -r fb5d8a50c641 -r c9910404cc8a src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Wed Jun 22 10:09:20 2016 +0200
+++ b/src/Pure/Isar/generic_target.ML	Wed Jun 22 10:40:53 2016 +0200
@@ -241,8 +241,8 @@
       |> foundation (((b, U), mx'), (b_def, rhs')) (type_params, term_params);
 
     (*local definition*)
-    val ((lhs, local_def), lthy3) = lthy2
-      |> Local_Defs.add_def ((b, NoSyn), lhs');
+    val ([(lhs, (_, local_def))], lthy3) = lthy2
+      |> Local_Defs.define [((b, NoSyn), (Thm.empty_binding, lhs'))];
 
     (*result*)
     val def =
diff -r fb5d8a50c641 -r c9910404cc8a src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Wed Jun 22 10:09:20 2016 +0200
+++ b/src/Pure/Isar/local_defs.ML	Wed Jun 22 10:40:53 2016 +0200
@@ -10,9 +10,8 @@
   val abs_def: term -> (string * typ) * term
   val expand: cterm list -> thm -> thm
   val def_export: Assumption.export
-  val add_defs: ((binding * mixfix) * (Thm.binding * term)) list -> Proof.context ->
+  val define: ((binding * mixfix) * (Thm.binding * term)) list -> Proof.context ->
     (term * (string * thm)) list * Proof.context
-  val add_def: (binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
   val fixed_abbrev: (binding * mixfix) * term -> Proof.context ->
     (term * term) * Proof.context
   val export: Proof.context -> Proof.context -> thm -> (thm list * thm list) * thm
@@ -66,7 +65,9 @@
   let
     val (bs, rhss) = split_list args;
     val Ts = map Term.fastype_of rhss;
-    val (xs, _) = Proof_Context.add_fixes (map2 (fn b => fn T => (b, SOME T, NoSyn)) bs Ts) ctxt;
+    val (xs, _) = ctxt
+      |> Context_Position.set_visible false
+      |> Proof_Context.add_fixes (map2 (fn b => fn T => (b, SOME T, NoSyn)) bs Ts);
     val lhss = ListPair.map Free (xs, Ts);
   in map Logic.mk_equals (lhss ~~ rhss) end;
 
@@ -94,13 +95,13 @@
 fun def_export _ defs = (expand defs, expand_term defs);
 
 
-(* add defs *)
+(* define *)
 
-fun add_defs defs ctxt =
+fun define defs ctxt =
   let
     val ((xs, mxs), specs) = defs |> split_list |>> split_list;
     val (bs, rhss) = specs |> split_list;
-    val eqs = mk_def (Context_Position.set_visible false ctxt) (xs ~~ rhss);
+    val eqs = mk_def ctxt (xs ~~ rhss);
     val lhss = map (fst o Logic.dest_equals) eqs;
   in
     ctxt
@@ -110,10 +111,6 @@
     |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss
   end;
 
-fun add_def (var, rhs) ctxt =
-  let val ([(lhs, (_, th))], ctxt') = add_defs [(var, (Thm.empty_binding, rhs))] ctxt
-  in ((lhs, th), ctxt') end;
-
 
 (* fixed_abbrev *)
 
diff -r fb5d8a50c641 -r c9910404cc8a src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jun 22 10:09:20 2016 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Jun 22 10:40:53 2016 +0200
@@ -699,7 +699,7 @@
         let
           val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) =>
             ((x, mx), ((Thm.def_binding_optional x a, atts), rhs)));
-        in map_context_result (Local_Defs.add_defs defs) end))
+        in map_context_result (Local_Defs.define defs) end))
     |-> (set_facts o map (#2 o #2))
   end;
 
@@ -868,7 +868,7 @@
     val derived_def = Local_Defs.derived_def ctxt {conditional = false};
     val defs1 = map (derived_def o Logic.close_prop (map #2 fixes) []) (flat propss);
     val defs2 = match_defs decls defs1;
-    val (defs3, defs_ctxt) = Local_Defs.add_defs defs2 ctxt;
+    val (defs3, defs_ctxt) = Local_Defs.define defs2 ctxt;
 
     (*notes*)
     val def_thmss =
diff -r fb5d8a50c641 -r c9910404cc8a src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed Jun 22 10:09:20 2016 +0200
+++ b/src/Tools/induct.ML	Wed Jun 22 10:40:53 2016 +0200
@@ -725,7 +725,7 @@
     fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt)
       | add (SOME (SOME x, (t, _))) ctxt =
           let val ([(lhs, (_, th))], ctxt') =
-            Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))] ctxt
+            Local_Defs.define [((x, NoSyn), ((Thm.def_binding x, []), t))] ctxt
           in ((SOME lhs, [th]), ctxt') end
       | add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
       | add (SOME (NONE, (t, _))) ctxt =
@@ -733,7 +733,7 @@
             val (s, _) = Name.variant "x" (Variable.names_of ctxt);
             val x = Binding.name s;
             val ([(lhs, (_, th))], ctxt') = ctxt
-              |> Local_Defs.add_defs [((x, NoSyn), ((Thm.def_binding x, []), t))];
+              |> Local_Defs.define [((x, NoSyn), ((Thm.def_binding x, []), t))];
           in ((SOME lhs, [th]), ctxt') end
       | add NONE ctxt = ((NONE, []), ctxt);
   in fold_map add def_insts #> apfst (split_list #> apsnd flat) end;