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 *)