# HG changeset patch
# User wenzelm
# Date 1238269972 -3600
# Node ID dca52e22913868267fbd7ecab412b2080b7bca18
# Parent  a06b4404632837485c97eb79e69136194fc105d2# Parent  3e3e7aa0cc7a86980d13332d569612da71bc628c
merged

diff -r a06b44046328 -r dca52e229138 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -181,7 +181,7 @@
       | xs => error ("No such case(s) in inductive definition: " ^ commas_quote xs));
     fun mk_avoids params name sets =
       let
-        val (_, ctxt') = ProofContext.add_fixes_i
+        val (_, ctxt') = ProofContext.add_fixes
           (map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params) ctxt;
         fun mk s =
           let
diff -r a06b44046328 -r dca52e229138 src/HOL/Tools/function_package/fundef_lib.ML
--- a/src/HOL/Tools/function_package/fundef_lib.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -55,7 +55,7 @@
 fun dest_all_all_ctx ctx (Const ("all", _) $ Abs (a as (n,T,b))) =
     let
       val [(n', _)] = Variable.variant_frees ctx [] [(n,T)]
-      val (_, ctx') = ProofContext.add_fixes_i [(Binding.name n', SOME T, NoSyn)] ctx
+      val (_, ctx') = ProofContext.add_fixes [(Binding.name n', SOME T, NoSyn)] ctx
 
       val (n'', body) = Term.dest_abs (n', T, b) 
       val _ = (n' = n'') orelse error "dest_all_ctx"
diff -r a06b44046328 -r dca52e229138 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -156,9 +156,9 @@
         val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
     in
       lthy
-        |> ProofContext.note_thmss_i "" [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
-        |> ProofContext.note_thmss_i "" [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
-        |> ProofContext.note_thmss_i ""
+        |> ProofContext.note_thmss "" [((Binding.empty, [ContextRules.rule_del]), [([allI], [])])] |> snd
+        |> ProofContext.note_thmss "" [((Binding.empty, [ContextRules.intro_bang (SOME 1)]), [([allI], [])])] |> snd
+        |> ProofContext.note_thmss ""
           [((Binding.name "termination", [ContextRules.intro_bang (SOME 0)]),
             [([Goal.norm_result termination], [])])] |> snd
         |> Proof.theorem_i NONE (total_termination_afterqed data) [[(goal, [])]]
diff -r a06b44046328 -r dca52e229138 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/Pure/Isar/attrib.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -18,10 +18,13 @@
   val attribute_i: theory -> src -> attribute
   val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
   val map_specs: ('a -> 'att) ->
-    (('c * 'a list) * 'd) list -> (('c * 'att list) * 'd) list
+    (('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
   val map_facts: ('a -> 'att) ->
     (('c * 'a list) * ('d * 'a list) list) list ->
     (('c * 'att list) * ('d * 'att list) list) list
+  val map_facts_refs: ('a -> 'att) -> ('b -> 'fact) ->
+    (('c * 'a list) * ('b * 'a list) list) list ->
+    (('c * 'att list) * ('fact * 'att list) list) list
   val crude_closure: Proof.context -> src -> src
   val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
   val syntax: attribute context_parser -> src -> attribute
@@ -121,14 +124,17 @@
 fun attribute thy = attribute_i thy o intern_src thy;
 
 fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
-    [(Thm.empty_binding, map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
+    [(Thm.empty_binding, args |> map (fn (a, atts) =>
+        (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
   |> fst |> maps snd;
 
 
 (* attributed declarations *)
 
 fun map_specs f = map (apfst (apsnd (map f)));
+
 fun map_facts f = map (apfst (apsnd (map f)) o apsnd (map (apsnd (map f))));
+fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
 
 
 (* crude_closure *)
diff -r a06b44046328 -r dca52e229138 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/Pure/Isar/class.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -225,8 +225,9 @@
       |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
     val all_params = Locale.params_of thy class;
     val raw_params = (snd o chop (length supparams)) all_params;
-    fun add_const (b, SOME raw_ty, _) thy =
+    fun add_const ((raw_c, raw_ty), _) thy =
       let
+        val b = Binding.name raw_c;
         val c = Sign.full_name thy b;
         val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
         val ty0 = Type.strip_sorts ty;
@@ -284,7 +285,7 @@
        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     #-> (fn (base_morph, morph, export_morph, axiom, assm_intro, of_class) =>
        Locale.add_registration (class, (morph, export_morph))
-    #> Locale.activate_global_facts (class, morph $> export_morph)
+    #> Context.theory_map (Locale.activate_facts (class, morph $> export_morph))
     #> register class sups params base_sort base_morph axiom assm_intro of_class))
     |> TheoryTarget.init (SOME class)
     |> pair class
diff -r a06b44046328 -r dca52e229138 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/Pure/Isar/class_target.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -287,8 +287,8 @@
     |> fold (fn dep_morph => Locale.add_dependency sub (sup,
         dep_morph $> Element.satisfy_morphism (the_list some_wit) $> export))
           (the_list some_dep_morph)
-    |> (fn thy => fold_rev Locale.activate_global_facts
-      (Locale.get_registrations thy) thy)
+    |> (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
+        (Locale.get_registrations thy) thy)
   end;
 
 
diff -r a06b44046328 -r dca52e229138 src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -25,13 +25,13 @@
     fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
 
     val thy_ctxt = ProofContext.init thy;
-    val struct_ctxt = #2 (ProofContext.add_fixes_i structs thy_ctxt);
+    val struct_ctxt = #2 (ProofContext.add_fixes structs thy_ctxt);
     val ((d, mx), var_ctxt) =
       (case raw_decl of
         NONE => ((NONE, NoSyn), struct_ctxt)
       | SOME raw_var =>
           struct_ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] =>
-            ProofContext.add_fixes_i [(x, T, mx)] #> snd #> pair (SOME x, mx)));
+            ProofContext.add_fixes [(x, T, mx)] #> snd #> pair (SOME x, mx)));
 
     val prop = prep_prop var_ctxt raw_prop;
     val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
diff -r a06b44046328 -r dca52e229138 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/Pure/Isar/element.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -486,7 +486,7 @@
 local
 
 fun activate_elem (Fixes fixes) ctxt =
-      ctxt |> ProofContext.add_fixes_i fixes |> snd
+      ctxt |> ProofContext.add_fixes fixes |> snd
   | activate_elem (Constrains _) ctxt =
       ctxt
   | activate_elem (Assumes asms) ctxt =
@@ -510,7 +510,7 @@
   | activate_elem (Notes (kind, facts)) ctxt =
       let
         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
-        val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
+        val (res, ctxt') = ctxt |> ProofContext.note_thmss kind facts';
       in ctxt' end;
 
 fun gen_activate prep_facts raw_elems ctxt =
diff -r a06b44046328 -r dca52e229138 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -20,14 +20,14 @@
 
   (* Declaring locales *)
   val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list ->
-    Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
+    Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
       * Element.context_i list) * ((string * typ) list * Proof.context)
   val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list ->
-    Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
+    Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
       * Element.context_i list) * ((string * typ) list * Proof.context)
       (*FIXME*)
   val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
-    Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
+    Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
       * Element.context_i list) * ((string * typ) list * Proof.context)
   val add_locale: binding -> binding -> expression_i -> Element.context_i list ->
     theory -> string * local_theory
@@ -80,22 +80,17 @@
 fun parameters_of thy strict (expr, fixed) =
   let
     fun reject_dups message xs =
-      let val dups = duplicates (op =) xs
-      in
-        if null dups then () else error (message ^ commas dups)
-      end;
+      (case duplicates (op =) xs of
+        [] => ()
+      | dups => error (message ^ commas dups));
 
-    fun match_bind (n, b) = (n = Binding.name_of b);
-    fun parm_eq ((b1, mx1: mixfix), (b2, mx2)) =
-      Binding.eq_name (b1, b2) andalso
-        (mx1 = mx2 orelse
-          error ("Conflicting syntax for parameter " ^ quote (Binding.str_of b1) ^ " in expression"));
+    fun parm_eq ((p1: string, mx1: mixfix), (p2, mx2)) = p1 = p2 andalso
+      (mx1 = mx2 orelse error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression"));
 
-    fun params_loc loc =
-      (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
+    fun params_loc loc = Locale.params_of thy loc |> map (apfst #1);
     fun params_inst (expr as (loc, (prfx, Positional insts))) =
           let
-            val (ps, loc') = params_loc loc;
+            val ps = params_loc loc;
             val d = length ps - length insts;
             val insts' =
               if d < 0 then error ("More arguments than parameters in instantiation of locale " ^
@@ -103,17 +98,17 @@
               else insts @ replicate d NONE;
             val ps' = (ps ~~ insts') |>
               map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
-          in (ps', (loc', (prfx, Positional insts'))) end
+          in (ps', (loc, (prfx, Positional insts'))) end
       | params_inst (expr as (loc, (prfx, Named insts))) =
           let
             val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
               (map fst insts);
 
-            val (ps, loc') = params_loc loc;
+            val ps = params_loc loc;
             val ps' = fold (fn (p, _) => fn ps =>
-              if AList.defined match_bind ps p then AList.delete match_bind p ps
-              else error (quote p ^" not a parameter of instantiated expression.")) insts ps;
-          in (ps', (loc', (prfx, Named insts))) end;
+              if AList.defined (op =) ps p then AList.delete (op =) p ps
+              else error (quote p ^ " not a parameter of instantiated expression")) insts ps;
+          in (ps', (loc, (prfx, Named insts))) end;
     fun params_expr is =
           let
             val (is', ps') = fold_map (fn i => fn ps =>
@@ -125,7 +120,7 @@
 
     val (implicit, expr') = params_expr expr;
 
-    val implicit' = map (#1 #> Name.of_binding) implicit;
+    val implicit' = map #1 implicit;
     val fixed' = map (#1 #> Name.of_binding) fixed;
     val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
     val implicit'' =
@@ -133,7 +128,7 @@
       else
         let val _ = reject_dups
           "Parameter(s) declared simultaneously in expression and for clause: " (implicit' @ fixed')
-        in map (fn (b, mx) => (b, NONE, mx)) implicit end;
+        in map (fn (x, mx) => (Binding.name x, NONE, mx)) implicit end;
 
   in (expr', implicit'' @ fixed) end;
 
@@ -276,7 +271,7 @@
 
 fun declare_elem prep_vars (Fixes fixes) ctxt =
       let val (vars, _) = prep_vars fixes ctxt
-      in ctxt |> ProofContext.add_fixes_i vars |> snd end
+      in ctxt |> ProofContext.add_fixes vars |> snd end
   | declare_elem prep_vars (Constrains csts) ctxt =
       ctxt |> prep_vars (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) csts) |> snd
   | declare_elem _ (Assumes _) ctxt = ctxt
@@ -319,8 +314,7 @@
 fun finish_inst ctxt parms do_close (loc, (prfx, inst)) =
   let
     val thy = ProofContext.theory_of ctxt;
-    val (parm_names, parm_types) = Locale.params_of thy loc |>
-      map_split (fn (b, SOME T, _) => (Binding.name_of b, T));
+    val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
     val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
   in (loc, morph) end;
 
@@ -349,9 +343,7 @@
 
     fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
       let
-        val (parm_names, parm_types) = Locale.params_of thy loc |>
-          map_split (fn (b, SOME T, _) => (Name.of_binding b, T))
-            (*FIXME return value of Locale.params_of has strange type*)
+        val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
         val inst' = prep_inst ctxt parm_names inst;
         val parm_types' = map (TypeInfer.paramify_vars o
           Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
@@ -360,7 +352,7 @@
         val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
         val inst''' = insts'' |> List.last |> snd |> snd;
         val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
-        val ctxt'' = Locale.activate_declarations thy (loc, morph) ctxt;
+        val ctxt'' = Locale.activate_declarations (loc, morph) ctxt;
       in (i + 1, insts', ctxt'') end;
 
     fun prep_elem insts raw_elem (elems, ctxt) =
@@ -376,7 +368,7 @@
       in check_autofix insts elems concl ctxt end;
 
     val fors = prep_vars_inst fixed ctxt1 |> fst;
-    val ctxt2 = ctxt1 |> ProofContext.add_fixes_i fors |> snd;
+    val ctxt2 = ctxt1 |> ProofContext.add_fixes fors |> snd;
     val (_, insts', ctxt3) = fold prep_insts raw_insts (0, [], ctxt2);
     val ctxt4 = init_body ctxt3;
     val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
@@ -390,9 +382,10 @@
     val parms = xs ~~ Ts;  (* params from expression and elements *)
 
     val Fixes fors' = finish_primitive parms I (Fixes fors);
+    val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';
     val (deps, elems'') = finish ctxt6 parms do_close insts elems';
 
-  in ((fors', deps, elems'', concl), (parms, ctxt7)) end
+  in ((fixed, deps, elems'', concl), (parms, ctxt7)) end
 
 in
 
@@ -432,6 +425,9 @@
 
 (* Locale declaration: import + elements *)
 
+fun fix_params params =
+  ProofContext.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
+
 local
 
 fun prep_declaration prep activate raw_import init_body raw_elems context =
@@ -440,8 +436,8 @@
       prep false true raw_import init_body raw_elems [] context ;
     (* Declare parameters and imported facts *)
     val context' = context |>
-      ProofContext.add_fixes_i fixed |> snd |>
-      fold Locale.activate_local_facts deps;
+      fix_params fixed |>
+      fold (Context.proof_map o Locale.activate_facts) deps;
     val (elems', _) = context' |>
       ProofContext.set_stmt true |>
       activate elems;
@@ -477,7 +473,7 @@
     val propss = map (props_of thy) deps;
 
     val goal_ctxt = context |>
-      ProofContext.add_fixes_i fixed |> snd |>
+      fix_params fixed |>
       (fold o fold) Variable.auto_fixes propss;
 
     val export = Variable.export_morphism goal_ctxt context;
@@ -658,13 +654,13 @@
 
 fun define_preds pname parms (((exts, exts'), (ints, ints')), defs) thy =
   let
-    val defs' = map (cterm_of thy #> Assumption.assume #> Drule.gen_all #> Drule.abs_def) defs;
+    val defs' = map (cterm_of thy #> Assumption.assume #> Drule.abs_def) defs;
 
     val (a_pred, a_intro, a_axioms, thy'') =
       if null exts then (NONE, NONE, [], thy)
       else
         let
-          val aname = if null ints then pname else Binding.suffix_name ("_" ^ axiomsN) pname
+          val aname = if null ints then pname else Binding.suffix_name ("_" ^ axiomsN) pname;
           val ((statement, intro, axioms), thy') =
             thy
             |> def_pred aname parms defs' exts exts';
@@ -737,7 +733,8 @@
     val b_satisfy = Element.satisfy_morphism b_axioms;
 
     val params = fixed @
-      (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
+      maps (fn Fixes fixes =>
+        map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fixes | _ => []) body_elems;
     val asm = if is_some b_statement then b_statement else a_statement;
 
     val notes =
@@ -790,7 +787,7 @@
     fun after_qed witss = ProofContext.theory
       (fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
         (name, morph $> Element.satisfy_morphism wits $> export)) deps witss #>
-      (fn thy => fold_rev Locale.activate_global_facts
+      (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
         (Locale.get_registrations thy) thy));
   in Element.witness_proof after_qed propss goal_ctxt end;
 
@@ -830,7 +827,7 @@
     fun store_eqns_activate regs [] thy =
           thy
           |> fold (fn (name, morph) =>
-               Locale.activate_global_facts (name, morph $> export)) regs
+               Context.theory_map (Locale.activate_facts (name, morph $> export))) regs
       | store_eqns_activate regs eqs thy =
           let
             val eqs' = eqs |> map (Morphism.thm (export' $> export) #>
@@ -842,7 +839,7 @@
             thy
             |> fold (fn (name, morph) =>
                 Locale.amend_registration eq_morph (name, morph) #>
-                Locale.activate_global_facts (name, morph $> eq_morph $> export)) regs
+                Context.theory_map (Locale.activate_facts (name, morph $> eq_morph $> export))) regs
             |> PureThy.note_thmss Thm.lemmaK (eq_attns' ~~ map (fn eq => [([eq], [])]) eqs')
             |> snd
           end;
@@ -876,7 +873,7 @@
     fun store_reg (name, morph) thms =
       let
         val morph' = morph $> Element.satisfy_morphism thms $> export;
-      in Locale.activate_local_facts (name, morph') end;
+      in Context.proof_map (Locale.activate_facts (name, morph')) end;
 
     fun after_qed wits =
       Proof.map_context (fold2 store_reg regs wits);
diff -r a06b44046328 -r dca52e229138 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -96,7 +96,7 @@
     val lhss = map (fst o Logic.dest_equals) eqs;
   in
     ctxt
-    |> ProofContext.add_fixes_i (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
+    |> ProofContext.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) bvars mxs) |> #2
     |> fold Variable.declare_term eqs
     |> ProofContext.add_assms_i def_export
       (map2 (fn a => fn eq => (a, [(eq, [])])) (names ~~ atts) eqs)
@@ -115,7 +115,7 @@
     val T = Term.fastype_of rhs;
     val ([x'], ctxt') = ctxt
       |> Variable.declare_term rhs
-      |> ProofContext.add_fixes_i [(x, SOME T, mx)];
+      |> ProofContext.add_fixes [(x, SOME T, mx)];
     val lhs = Free (x', T);
     val _ = cert_def ctxt' (Logic.mk_equals (lhs, rhs));
     fun abbrev_export _ _ = (I, Envir.expand_term_frees [((x', T), rhs)]);
diff -r a06b44046328 -r dca52e229138 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -30,7 +30,7 @@
 sig
   (* Locale specification *)
   val register_locale: binding ->
-    (string * sort) list * (binding * typ option * mixfix) list ->
+    (string * sort) list * ((string * typ) * mixfix) list ->
     term option * term list ->
     thm option * thm option -> thm list ->
     declaration list * declaration list ->
@@ -39,7 +39,7 @@
   val intern: theory -> xstring -> string
   val extern: theory -> string -> xstring
   val defined: theory -> string -> bool
-  val params_of: theory -> string -> (binding * typ option * mixfix) list
+  val params_of: theory -> string -> ((string * typ) * mixfix) list
   val intros_of: theory -> string -> thm option * thm option
   val axioms_of: theory -> string -> thm list
   val instance_of: theory -> string -> morphism -> term list
@@ -56,10 +56,8 @@
   val add_dependency: string -> string * morphism -> theory -> theory
 
   (* Activation *)
-  val activate_declarations: theory -> string * morphism ->
-    Proof.context -> Proof.context
-  val activate_global_facts: string * morphism -> theory -> theory
-  val activate_local_facts: string * morphism -> Proof.context -> Proof.context
+  val activate_declarations: string * morphism -> Proof.context -> Proof.context
+  val activate_facts: string * morphism -> Context.generic -> Context.generic
   val init: string -> theory -> Proof.context
 
   (* Reasoning about locales *)
@@ -91,7 +89,7 @@
 
 datatype locale = Loc of {
   (** static part **)
-  parameters: (string * sort) list * (binding * typ option * mixfix) list,
+  parameters: (string * sort) list * ((string * typ) * mixfix) list,
     (* type and term parameters *)
   spec: term option * term list,
     (* assumptions (as a single predicate expression) and defines *)
@@ -109,8 +107,10 @@
 fun mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies)) =
   Loc {parameters = parameters, intros = intros, axioms = axioms, spec = spec,
     decls = decls, notes = notes, dependencies = dependencies};
+
 fun map_locale f (Loc {parameters, spec, intros, axioms, decls, notes, dependencies}) =
   mk_locale (f ((parameters, spec, intros, axioms), ((decls, notes), dependencies)));
+
 fun merge_locale (Loc {parameters, spec, intros, axioms, decls = (decls1, decls2),
   notes, dependencies}, Loc {decls = (decls1', decls2'), notes = notes',
     dependencies = dependencies', ...}) = mk_locale
@@ -163,7 +163,7 @@
 fun axioms_of thy = #axioms o the_locale thy;
 
 fun instance_of thy name morph = params_of thy name |>
-  map (fn (b, T, _) => Morphism.term morph (Free (Name.of_binding b, the T)));
+  map (Morphism.term morph o Free o #1);
 
 fun specification_of thy = #spec o the_locale thy;
 
@@ -178,26 +178,20 @@
 
 (** Identifiers: activated locales in theory or proof context **)
 
-type identifiers = (string * term list) list;
-
-val empty = ([] : identifiers);
-
 fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
 
 local
 
-datatype 'a delayed = Ready of 'a | ToDo of ('a delayed * 'a delayed);
+datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
 
 structure Identifiers = GenericDataFun
 (
-  type T = identifiers delayed;
-  val empty = Ready empty;
+  type T = (string * term list) list delayed;
+  val empty = Ready [];
   val extend = I;
   fun merge _ = ToDo;
 );
 
-in
-
 fun finish thy (ToDo (i1, i2)) = merge (ident_eq thy) (finish thy i1, finish thy i2)
   | finish _ (Ready ids) = ids;
 
@@ -206,13 +200,10 @@
     Ready _ => NONE
   | ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy)))));
 
-fun get_global_idents thy =
-  let val (Ready ids) = (Identifiers.get o Context.Theory) thy in ids end;
-val put_global_idents = Context.theory_map o Identifiers.put o Ready;
+in
 
-fun get_local_idents ctxt =
-  let val (Ready ids) = (Identifiers.get o Context.Proof) ctxt in ids end;
-val put_local_idents = Context.proof_map o Identifiers.put o Ready;
+val get_idents = (fn Ready ids => ids) o Identifiers.get;
+val put_idents = Identifiers.put o Ready;
 
 end;
 
@@ -228,15 +219,14 @@
   then error "Roundup bound exceeded (sublocale relation probably not terminating)."
   else
     let
-      val {parameters = (_, params), dependencies, ...} = the_locale thy name;
+      val dependencies = dependencies_of thy name;
       val instance = instance_of thy name morph;
     in
       if member (ident_eq thy) marked (name, instance)
       then (deps, marked)
       else
         let
-          val dependencies' =
-            map (fn ((name, morph'), _) => (name, morph' $>  morph)) dependencies;
+          val dependencies' = map (fn (name, morph') => (name, morph' $> morph)) dependencies;
           val marked' = (name, instance) :: marked;
           val (deps', marked'') = fold_rev (add thy (depth + 1)) dependencies' ([], marked');
         in
@@ -250,7 +240,7 @@
   let
     (* Find all dependencies incuding new ones (which are dependencies enriching
       existing registrations). *)
-    val (dependencies, marked') = add thy 0 (name, morph) ([], empty);
+    val (dependencies, marked') = add thy 0 (name, morph) ([], []);
     (* Filter out exisiting fragments. *)
     val dependencies' = filter_out (fn (name, morph) =>
       member (ident_eq thy) marked (name, instance_of thy name morph)) dependencies;
@@ -263,12 +253,14 @@
 
 (* Declarations, facts and entire locale content *)
 
-fun activate_decls thy (name, morph) ctxt =
+fun activate_decls (name, morph) context =
   let
+    val thy = Context.theory_of context;
     val {decls = (typ_decls, term_decls), ...} = the_locale thy name;
   in
-    ctxt |> fold_rev (fn (decl, _) => Context.proof_map (decl morph)) typ_decls |>
-      fold_rev (fn (decl, _) => Context.proof_map (decl morph)) term_decls
+    context
+    |> fold_rev (fn (decl, _) => decl morph) typ_decls
+    |> fold_rev (fn (decl, _) => decl morph) term_decls
   end;
 
 fun activate_notes activ_elem transfer thy (name, morph) input =
@@ -284,17 +276,17 @@
 
 fun activate_all name thy activ_elem transfer (marked, input) =
   let
-    val {parameters = (_, params), spec = (asm, defs), ...} =
-      the_locale thy name;
-  in
-    input |>
-      (if not (null params) then activ_elem (Fixes params) else I) |>
+    val {parameters = (_, params), spec = (asm, defs), ...} = the_locale thy name;
+    val input' = input |>
+      (not (null params) ?
+        activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
       (* FIXME type parameters *)
-      (if is_some asm then activ_elem (Assumes [(Attrib.empty_binding, [(the asm, [])])]) else I) |>
+      (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
       (if not (null defs)
         then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
-        else I) |>
-      pair marked |> roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity)
+        else I);
+  in
+    roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity) (marked, input')
   end;
 
 
@@ -302,64 +294,65 @@
 
 local
 
-fun init_global_elem (Notes (kind, facts)) thy =
-  let
-    val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
-  in PureThy.note_thmss kind facts' thy |> snd end
-
-fun init_local_elem (Fixes fixes) ctxt = ctxt |>
-      ProofContext.add_fixes_i fixes |> snd
-  | init_local_elem (Assumes assms) ctxt =
+fun init_elem (Fixes fixes) (Context.Proof ctxt) =
+      Context.Proof (ProofContext.add_fixes fixes ctxt |> snd)
+  | init_elem (Assumes assms) (Context.Proof ctxt) =
       let
-        val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms
-      in
-        ctxt |> fold Variable.auto_fixes (maps (map fst o snd) assms') |>
-          ProofContext.add_assms_i Assumption.assume_export assms' |> snd
-     end
-  | init_local_elem (Defines defs) ctxt =
+        val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms;
+        val ctxt' = ctxt
+          |> fold Variable.auto_fixes (maps (map fst o snd) assms')
+          |> ProofContext.add_assms_i Assumption.assume_export assms' |> snd;
+      in Context.Proof ctxt' end
+  | init_elem (Defines defs) (Context.Proof ctxt) =
       let
-        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs
-      in
-        ctxt |> fold Variable.auto_fixes (map (fst o snd) defs') |>
-          ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs') |>
-          snd
-      end
-  | init_local_elem (Notes (kind, facts)) ctxt =
+        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
+        val ctxt' = ctxt
+          |> fold Variable.auto_fixes (map (fst o snd) defs')
+          |> ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs')
+          |> snd;
+      in Context.Proof ctxt' end
+  | init_elem (Notes (kind, facts)) (Context.Proof ctxt) =
       let
         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
-      in ProofContext.note_thmss_i kind facts' ctxt |> snd end
-
-fun cons_elem false (Notes notes) elems = elems
-  | cons_elem _ elem elems = elem :: elems
+      in Context.Proof (ProofContext.note_thmss kind facts' ctxt |> snd) end
+  | init_elem (Notes (kind, facts)) (Context.Theory thy) =
+      let
+        val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
+      in Context.Theory (PureThy.note_thmss kind facts' thy |> snd) end
+  | init_elem _ (Context.Theory _) = raise Fail "Bad context element in global theory";
 
 in
 
-fun activate_declarations thy dep ctxt =
-  roundup thy activate_decls dep (get_local_idents ctxt, ctxt) |-> put_local_idents;
+fun activate_declarations dep ctxt =
+  let
+    val context = Context.Proof ctxt;
+    val thy = Context.theory_of context;
+    val context' = roundup thy (K activate_decls) dep (get_idents context, context) |-> put_idents;
+  in Context.the_proof context' end;
 
-fun activate_global_facts dep thy =
-  roundup thy (activate_notes init_global_elem Element.transfer_morphism)
-    dep (get_global_idents thy, thy) |-> put_global_idents;
-
-fun activate_local_facts dep ctxt =
-  roundup (ProofContext.theory_of ctxt)
-  (activate_notes init_local_elem (Element.transfer_morphism o ProofContext.theory_of)) dep
-    (get_local_idents ctxt, ctxt) |-> put_local_idents;
+fun activate_facts dep context =
+  let
+    val thy = Context.theory_of context;
+    val activate = activate_notes init_elem (Element.transfer_morphism o Context.theory_of);
+  in roundup thy activate dep (get_idents context, context) |-> put_idents end;
 
 fun init name thy =
-  activate_all name thy init_local_elem (Element.transfer_morphism o ProofContext.theory_of)
-    (empty, ProofContext.init thy) |-> put_local_idents;
+  activate_all name thy init_elem (Element.transfer_morphism o Context.theory_of)
+    ([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;
 
-fun print_locale thy show_facts name =
+fun print_locale thy show_facts raw_name =
   let
-    val name' = intern thy name;
-    val ctxt = init name' thy
+    val name = intern thy raw_name;
+    val ctxt = init name thy;
+    fun cons_elem (elem as Notes _) = show_facts ? cons elem
+      | cons_elem elem = cons elem;
+    val elems =
+      activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], [])
+      |> snd |> rev;
   in
-    Pretty.big_list "locale elements:"
-      (activate_all name' thy (cons_elem show_facts) (K (Element.transfer_morphism thy))
-        (empty, []) |> snd |> rev |>
-        map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
-  end
+    Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
+    |> Pretty.writeln
+  end;
 
 end;
 
@@ -379,24 +372,25 @@
 );
 
 val get_registrations =
-  Registrations.get #> map fst #> map (apsnd op $>);
+  Registrations.get #> map (#1 #> apsnd op $>);
 
 fun add_registration (name, (base_morph, export)) thy =
   roundup thy (fn _ => fn (name', morph') =>
-    (Registrations.map o cons) ((name', (morph', export)), stamp ()))
-    (name, base_morph) (get_global_idents thy, thy) |> snd
-    (* FIXME |-> put_global_idents ?*);
+    Registrations.map (cons ((name', (morph', export)), stamp ())))
+    (name, base_morph) (get_idents (Context.Theory thy), thy) |> snd;
+    (* FIXME |-> put_global_idents ?*)
 
 fun amend_registration morph (name, base_morph) thy =
   let
-    val regs = (Registrations.get #> map fst) thy;
+    val regs = map #1 (Registrations.get thy);
     val base = instance_of thy name base_morph;
     fun match (name', (morph', _)) =
       name = name' andalso eq_list (op aconv) (base, instance_of thy name' morph');
     val i = find_index match (rev regs);
-    val _ = if i = ~1 then error ("No registration of locale " ^
+    val _ =
+      if i = ~1 then error ("No registration of locale " ^
         quote (extern thy name) ^ " and parameter instantiation " ^
-        space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available.")
+        space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^ " available")
       else ();
   in
     Registrations.map (nth_map (length regs - 1 - i)
diff -r a06b44046328 -r dca52e229138 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/Pure/Isar/obtain.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -118,7 +118,7 @@
 
     (*obtain vars*)
     val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
-    val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
+    val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes vars;
     val xs = map (Name.of_binding o #1) vars;
 
     (*obtain asms*)
@@ -294,7 +294,7 @@
         |> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
         |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
           (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
-        |> Proof.add_binds_i AutoBind.no_facts
+        |> Proof.bind_terms AutoBind.no_facts
       end;
 
     val goal = Var (("guess", 0), propT);
diff -r a06b44046328 -r dca52e229138 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -17,7 +17,7 @@
   val theory_of: state -> theory
   val map_context: (context -> context) -> state -> state
   val map_contexts: (context -> context) -> state -> state
-  val add_binds_i: (indexname * term option) list -> state -> state
+  val bind_terms: (indexname * term option) list -> state -> state
   val put_thms: bool -> string * thm list option -> state -> state
   val the_facts: state -> thm list
   val the_fact: state -> thm
@@ -204,7 +204,7 @@
 
 fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
 
-val add_binds_i = map_context o ProofContext.add_binds_i;
+val bind_terms = map_context o ProofContext.bind_terms;
 val put_thms = map_context oo ProofContext.put_thms;
 
 
@@ -531,15 +531,15 @@
 
 local
 
-fun gen_fix add_fixes args =
+fun gen_fix prep_vars args =
   assert_forward
-  #> map_context (snd o add_fixes args)
+  #> map_context (fn ctxt => snd (ProofContext.add_fixes (prep_vars ctxt args) ctxt))
   #> put_facts NONE;
 
 in
 
-val fix = gen_fix ProofContext.add_fixes;
-val fix_i = gen_fix ProofContext.add_fixes_i;
+val fix = gen_fix (fn ctxt => fn args => fst (ProofContext.read_vars args ctxt));
+val fix_i = gen_fix (K I);
 
 end;
 
@@ -620,29 +620,27 @@
 
 local
 
-fun gen_thmss note_ctxt more_facts opt_chain opt_result prep_atts args state =
+fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state =
   state
   |> assert_forward
-  |> map_context_result (note_ctxt (Attrib.map_facts (prep_atts (theory_of state)) args))
+  |> map_context_result (ProofContext.note_thmss ""
+    (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state)) args))
   |> these_factss (more_facts state)
   ||> opt_chain
   |> opt_result;
 
 in
 
-val note_thmss = gen_thmss (ProofContext.note_thmss "") (K []) I #2 Attrib.attribute;
-val note_thmss_i = gen_thmss (ProofContext.note_thmss_i "") (K []) I #2 (K I);
-
-val from_thmss =
-  gen_thmss (ProofContext.note_thmss "") (K []) chain #2 Attrib.attribute o no_binding;
-val from_thmss_i = gen_thmss (ProofContext.note_thmss_i "") (K []) chain #2 (K I) o no_binding;
+val note_thmss = gen_thmss (K []) I #2 Attrib.attribute ProofContext.get_fact;
+val note_thmss_i = gen_thmss (K []) I #2 (K I) (K I);
 
-val with_thmss =
-  gen_thmss (ProofContext.note_thmss "") the_facts chain #2 Attrib.attribute o no_binding;
-val with_thmss_i = gen_thmss (ProofContext.note_thmss_i "") the_facts chain #2 (K I) o no_binding;
+val from_thmss = gen_thmss (K []) chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
+val from_thmss_i = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
 
-val local_results =
-  gen_thmss (ProofContext.note_thmss_i "") (K []) I I (K I) o map (apsnd Thm.simple_fact);
+val with_thmss = gen_thmss the_facts chain #2 Attrib.attribute ProofContext.get_fact o no_binding;
+val with_thmss_i = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
+
+val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
 
 fun get_thmss state srcs = the_facts (note_thmss [((Binding.empty, []), srcs)] state);
 
@@ -653,11 +651,13 @@
 
 local
 
-fun gen_using f g note prep_atts args state =
+fun gen_using f g prep_atts prep_fact args state =
   state
   |> assert_backward
   |> map_context_result
-    (note "" (Attrib.map_facts (prep_atts (theory_of state)) (no_binding args)))
+    (ProofContext.note_thmss ""
+      (Attrib.map_facts_refs (prep_atts (theory_of state)) (prep_fact (context_of state))
+        (no_binding args)))
   |> (fn (named_facts, state') =>
     state' |> map_goal I (fn (statement, _, using, goal, before_qed, after_qed) =>
       let
@@ -671,10 +671,10 @@
 
 in
 
-val using = gen_using append_using (K (K I)) ProofContext.note_thmss Attrib.attribute;
-val using_i = gen_using append_using (K (K I)) ProofContext.note_thmss_i (K I);
-val unfolding = gen_using unfold_using unfold_goals ProofContext.note_thmss Attrib.attribute;
-val unfolding_i = gen_using unfold_using unfold_goals ProofContext.note_thmss_i (K I);
+val using = gen_using append_using (K (K I)) Attrib.attribute ProofContext.get_fact;
+val using_i = gen_using append_using (K (K I)) (K I) (K I);
+val unfolding = gen_using unfold_using unfold_goals Attrib.attribute ProofContext.get_fact;
+val unfolding_i = gen_using unfold_using unfold_goals (K I) (K I);
 
 end;
 
@@ -695,7 +695,7 @@
   in
     state'
     |> assume_i assumptions
-    |> add_binds_i AutoBind.no_facts
+    |> bind_terms AutoBind.no_facts
     |> `the_facts |-> (fn thms => note_thmss_i [((Binding.name name, []), [(thms, [])])])
   end;
 
diff -r a06b44046328 -r dca52e229138 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -70,8 +70,7 @@
   val export: Proof.context -> Proof.context -> thm list -> thm list
   val export_morphism: Proof.context -> Proof.context -> morphism
   val norm_export_morphism: Proof.context -> Proof.context -> morphism
-  val add_binds: (indexname * string option) list -> Proof.context -> Proof.context
-  val add_binds_i: (indexname * term option) list -> Proof.context -> Proof.context
+  val bind_terms: (indexname * term option) list -> Proof.context -> Proof.context
   val auto_bind_goal: term list -> Proof.context -> Proof.context
   val auto_bind_facts: term list -> Proof.context -> Proof.context
   val match_bind: bool -> (string list * string) list -> Proof.context -> term list * Proof.context
@@ -102,19 +101,15 @@
   val mandatory_path: string -> Proof.context -> Proof.context
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val reset_naming: Proof.context -> Proof.context
-  val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
-    Proof.context -> (string * thm list) list * Proof.context
-  val note_thmss_i: string -> (Thm.binding * (thm list * attribute list) list) list ->
+  val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
   val read_vars: (binding * string option * mixfix) list -> Proof.context ->
     (binding * typ option * mixfix) list * Proof.context
   val cert_vars: (binding * typ option * mixfix) list -> Proof.context ->
     (binding * typ option * mixfix) list * Proof.context
-  val add_fixes: (binding * string option * mixfix) list ->
-    Proof.context -> string list * Proof.context
-  val add_fixes_i: (binding * typ option * mixfix) list ->
-    Proof.context -> string list * Proof.context
+  val add_fixes: (binding * typ option * mixfix) list -> Proof.context ->
+    string list * Proof.context
   val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
   val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
   val add_assms: Assumption.export ->
@@ -542,17 +537,17 @@
 
 local
 
-structure AllowDummies = ProofDataFun(type T = bool fun init _ = false);
+structure Allow_Dummies = ProofDataFun(type T = bool fun init _ = false);
 
 fun check_dummies ctxt t =
-  if AllowDummies.get ctxt then t
+  if Allow_Dummies.get ctxt then t
   else Term.no_dummy_patterns t handle TERM _ => error "Illegal dummy pattern(s) in term";
 
 fun prepare_dummies ts = #1 (fold_map Term.replace_dummy_patterns ts 1);
 
 in
 
-val allow_dummies = AllowDummies.put true;
+val allow_dummies = Allow_Dummies.put true;
 
 fun prepare_patterns ctxt =
   let val Mode {pattern, ...} = get_mode ctxt in
@@ -775,7 +770,7 @@
 
 
 
-(** bindings **)
+(** term bindings **)
 
 (* simult_matches *)
 
@@ -785,28 +780,23 @@
   | SOME (env, _) => map (apsnd snd) (Envir.alist_of env));
 
 
-(* add_binds(_i) *)
-
-local
+(* bind_terms *)
 
-fun gen_bind prep (xi as (x, _), raw_t) ctxt =
+val bind_terms = fold (fn (xi, t) => fn ctxt =>
   ctxt
-  |> Variable.add_binds [(xi, Option.map (prep (set_mode mode_default ctxt)) raw_t)];
+  |> Variable.bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t));
 
-in
+
+(* auto_bind *)
 
 fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
   | drop_schematic b = b;
 
-val add_binds = fold (gen_bind Syntax.read_term);
-val add_binds_i = fold (gen_bind cert_term);
+fun auto_bind f ts ctxt = ctxt |> bind_terms (map drop_schematic (f (theory_of ctxt) ts));
 
-fun auto_bind f ts ctxt = ctxt |> add_binds_i (map drop_schematic (f (theory_of ctxt) ts));
 val auto_bind_goal = auto_bind AutoBind.goal;
 val auto_bind_facts = auto_bind AutoBind.facts;
 
-end;
-
 
 (* match_bind(_i) *)
 
@@ -831,8 +821,8 @@
     val ctxt'' =
       tap (Variable.warn_extra_tfrees ctxt)
        (if gen then
-          ctxt (*sic!*) |> fold Variable.declare_term (map #2 binds') |> add_binds_i binds''
-        else ctxt' |> add_binds_i binds'');
+          ctxt (*sic!*) |> fold Variable.declare_term (map #2 binds') |> bind_terms binds''
+        else ctxt' |> bind_terms binds'');
   in (ts, ctxt'') end;
 
 in
@@ -868,8 +858,8 @@
 
     (*generalize result: context evaluated now, binds added later*)
     val gen = Variable.exportT_terms ctxt' ctxt;
-    fun gen_binds c = c |> add_binds_i (map #1 binds ~~ map SOME (gen (map #2 binds)));
-  in (ctxt' |> add_binds_i (map (apsnd SOME) binds), (propss, gen_binds)) end;
+    fun gen_binds c = c |> bind_terms (map #1 binds ~~ map SOME (gen (map #2 binds)));
+  in (ctxt' |> bind_terms (map (apsnd SOME) binds), (propss, gen_binds)) end;
 
 in
 
@@ -965,25 +955,23 @@
   | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
       (Facts.add_local do_props (naming_of ctxt) (b, ths) #> snd);
 
-fun gen_note_thmss get k = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
+in
+
+fun note_thmss kind = fold_map (fn ((b, more_attrs), raw_facts) => fn ctxt =>
   let
     val pos = Binding.pos_of b;
     val name = full_name ctxt b;
     val _ = ContextPosition.report_visible ctxt (Markup.local_fact_decl name) pos;
 
-    val facts = PureThy.name_thmss false pos name (map (apfst (get ctxt)) raw_facts);
+    val facts = PureThy.name_thmss false pos name raw_facts;
     fun app (th, attrs) x =
-      swap (Library.foldl_map (Thm.proof_attributes (surround (Thm.kind k) (attrs @ more_attrs))) (x, th));
+      swap (Library.foldl_map
+        (Thm.proof_attributes (surround (Thm.kind kind) (attrs @ more_attrs))) (x, th));
     val (res, ctxt') = fold_map app facts ctxt;
     val thms = PureThy.name_thms false false pos name (flat res);
     val Mode {stmt, ...} = get_mode ctxt;
   in ((name, thms), ctxt' |> update_thms stmt (b, SOME thms)) end);
 
-in
-
-fun note_thmss k = gen_note_thmss get_fact k;
-fun note_thmss_i k = gen_note_thmss (K I) k;
-
 fun put_thms do_props thms ctxt = ctxt
   |> map_naming (K local_naming)
   |> ContextPosition.set_visible false
@@ -1115,9 +1103,11 @@
     error ("Illegal mixfix syntax for internal/skolem constant " ^ quote x)
   else (true, (x, T, mx));
 
-fun gen_fixes prep raw_vars ctxt =
+in
+
+fun add_fixes raw_vars ctxt =
   let
-    val (vars, _) = prep raw_vars ctxt;
+    val (vars, _) = cert_vars raw_vars ctxt;
     val (xs', ctxt') = Variable.add_fixes (map (Name.of_binding o #1) vars) ctxt;
     val ctxt'' =
       ctxt'
@@ -1127,11 +1117,6 @@
       ContextPosition.report_visible ctxt (Markup.fixed_decl x') (Binding.pos_of b));
   in (xs', ctxt'') end;
 
-in
-
-val add_fixes = gen_fixes read_vars;
-val add_fixes_i = gen_fixes cert_vars;
-
 end;
 
 
@@ -1142,7 +1127,7 @@
 
 fun bind_fixes xs ctxt =
   let
-    val (_, ctxt') = ctxt |> add_fixes_i (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
+    val (_, ctxt') = ctxt |> add_fixes (map (fn x => (Binding.name x, NONE, NoSyn)) xs);
     fun bind (t as Free (x, T)) =
           if member (op =) xs x then
             (case lookup_skolem ctxt' x of SOME x' => Free (x', T) | NONE => t)
@@ -1167,7 +1152,7 @@
   in
     ctxt2
     |> auto_bind_facts (flat propss)
-    |> note_thmss_i Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss)
+    |> note_thmss Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss)
   end;
 
 in
@@ -1221,7 +1206,7 @@
     val RuleCases.Case {assumes, binds, cases, ...} = RuleCases.apply ts c;
   in
     ctxt'
-    |> add_binds_i (map drop_schematic binds)
+    |> bind_terms (map drop_schematic binds)
     |> add_cases true (map (apsnd SOME) cases)
     |> pair (assumes, (binds, cases))
   end;
diff -r a06b44046328 -r dca52e229138 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -283,7 +283,7 @@
         val (param_names, ctxt') = ctxt
           |> Variable.declare_thm thm
           |> Thm.fold_terms Variable.declare_constraints st
-          |> ProofContext.add_fixes_i (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
+          |> ProofContext.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
 
         (* Process type insts: Tinsts_env *)
         fun absent xi = error
diff -r a06b44046328 -r dca52e229138 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -108,7 +108,7 @@
     val thy = ProofContext.theory_of ctxt;
 
     val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
-    val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
+    val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes vars;
 
     val Asss = (map o map) (map (parse_prop params_ctxt) o snd) raw_specss;
     val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss)
@@ -312,7 +312,7 @@
               |> fold_map ProofContext.inferred_param xs;
             val asm = Term.list_all_free (xs ~~ Ts, Logic.list_implies (props, thesis));
           in
-            ctxt' |> (snd o ProofContext.add_fixes_i (map (fn b => (b, NONE, NoSyn)) bs));
+            ctxt' |> (snd o ProofContext.add_fixes (map (fn b => (b, NONE, NoSyn)) bs));
             ctxt' |> Variable.auto_fixes asm
             |> ProofContext.add_assms_i Assumption.assume_export
               [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
@@ -325,9 +325,9 @@
         val stmt = [((Binding.empty, atts), [(thesis, [])])];
 
         val (facts, goal_ctxt) = elems_ctxt
-          |> (snd o ProofContext.add_fixes_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)])
+          |> (snd o ProofContext.add_fixes [(Binding.name AutoBind.thesisN, NONE, NoSyn)])
           |> fold_map assume_case (obtains ~~ propp)
-          |-> (fn ths => ProofContext.note_thmss_i Thm.assumptionK
+          |-> (fn ths => ProofContext.note_thmss Thm.assumptionK
                 [((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
       in ((prems, stmt, facts), goal_ctxt) end);
 
@@ -370,7 +370,7 @@
       end;
   in
     goal_ctxt
-    |> ProofContext.note_thmss_i Thm.assumptionK
+    |> ProofContext.note_thmss Thm.assumptionK
       [((Binding.name AutoBind.assmsN, []), [(prems, [])])]
     |> snd
     |> Proof.theorem_i before_qed after_qed' (map snd stmt)
diff -r a06b44046328 -r dca52e229138 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -160,9 +160,9 @@
   in
     lthy |> LocalTheory.theory
       (PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd)
-    |> not is_locale ? LocalTheory.target (ProofContext.note_thmss_i kind global_facts #> snd)
+    |> not is_locale ? LocalTheory.target (ProofContext.note_thmss kind global_facts #> snd)
     |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
-    |> ProofContext.note_thmss_i kind local_facts
+    |> ProofContext.note_thmss kind local_facts
   end;
 
 
diff -r a06b44046328 -r dca52e229138 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -87,7 +87,7 @@
 val _ = macro "note" (Args.context :|-- (fn ctxt =>
   P.and_list1' (Scan.lift (Args.opt_thm_name I "=") -- Attrib.thms >> (fn ((a, srcs), ths) =>
     ((a, map (Attrib.attribute (ProofContext.theory_of ctxt)) srcs), [(ths, [])])))
-  >> (fn args => #2 (ProofContext.note_thmss_i "" args ctxt))));
+  >> (fn args => #2 (ProofContext.note_thmss "" args ctxt))));
 
 val _ = value "ctyp" (Args.typ >> (fn T =>
   "Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T)));
diff -r a06b44046328 -r dca52e229138 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sat Mar 28 18:18:01 2009 +0100
+++ b/src/Pure/variable.ML	Sat Mar 28 20:52:52 2009 +0100
@@ -30,7 +30,7 @@
   val declare_thm: thm -> Proof.context -> Proof.context
   val thm_context: thm -> Proof.context
   val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
-  val add_binds: (indexname * term option) list -> Proof.context -> Proof.context
+  val bind_term: indexname * term option -> Proof.context -> Proof.context
   val expand_binds: Proof.context -> term -> term
   val lookup_const: Proof.context -> string -> string option
   val is_const: Proof.context -> string -> bool
@@ -250,15 +250,13 @@
 
 (** term bindings **)
 
-fun add_bind (xi, NONE) = map_binds (Vartab.delete_safe xi)
-  | add_bind ((x, i), SOME t) =
+fun bind_term (xi, NONE) = map_binds (Vartab.delete_safe xi)
+  | bind_term ((x, i), SOME t) =
       let
         val u = Term.close_schematic_term t;
         val U = Term.fastype_of u;
       in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end;
 
-val add_binds = fold add_bind;
-
 fun expand_binds ctxt =
   let
     val binds = binds_of ctxt;
@@ -486,7 +484,7 @@
     val all_vars = Thm.fold_terms Term.add_vars st [];
     val no_binds = map (fn (xi, _) => (xi, NONE)) all_vars;
   in
-    add_binds no_binds #>
+    fold bind_term no_binds #>
     fold (declare_constraints o Var) all_vars #>
     focus (Thm.cprem_of st i)
   end;