# HG changeset patch
# User wenzelm
# Date 1427659090 -7200
# Node ID c7b7bca8592cf84846198346f5a37162ceeb7b23
# Parent  fafb4d12c30752d01c79e03e6f4fd0e9b5dc7a90
tuned signature;

diff -r fafb4d12c307 -r c7b7bca8592c src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sun Mar 29 21:47:16 2015 +0200
+++ b/src/Pure/Isar/element.ML	Sun Mar 29 21:58:10 2015 +0200
@@ -236,7 +236,7 @@
     val concl_term = Object_Logic.drop_judgment thy concl;
 
     val fixes = fold_aterms (fn v as Free (x, T) =>
-        if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
+        if Variable.is_newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
         then insert (op =) (Variable.revert_fixed ctxt' x, T) else I | _ => I) prop [] |> rev;
     val (assumes, cases) = take_suffix (fn prem =>
       is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
diff -r fafb4d12c307 -r c7b7bca8592c src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Sun Mar 29 21:47:16 2015 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Sun Mar 29 21:58:10 2015 +0200
@@ -239,9 +239,7 @@
       |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2
       |> read_insts thm mixed_insts;
 
-    fun add_fixed (Free (x, _)) = Variable.newly_fixed inst_ctxt goal_ctxt x ? insert (op =) x
-      | add_fixed _ = I;
-    val fixed = fold (Term.fold_aterms add_fixed o #2) inst_vars [];
+    val fixed = map #1 (fold (Variable.add_newly_fixed inst_ctxt goal_ctxt o #2) inst_vars []);
 
 
     (* lift and instantiate rule *)
diff -r fafb4d12c307 -r c7b7bca8592c src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sun Mar 29 21:47:16 2015 +0200
+++ b/src/Pure/variable.ML	Sun Mar 29 21:58:10 2015 +0200
@@ -38,7 +38,7 @@
   val restore_proper_fixes: Proof.context -> Proof.context -> Proof.context
   val is_improper: Proof.context -> string -> bool
   val is_fixed: Proof.context -> string -> bool
-  val newly_fixed: Proof.context -> Proof.context -> string -> bool
+  val is_newly_fixed: Proof.context -> Proof.context -> string -> bool
   val fixed_ord: Proof.context -> string * string -> order
   val intern_fixed: Proof.context -> string -> string
   val markup_fixed: Proof.context -> string -> Markup.T
@@ -46,6 +46,8 @@
   val revert_fixed: Proof.context -> string -> string
   val add_fixed_names: Proof.context -> term -> string list -> string list
   val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list
+  val add_newly_fixed: Proof.context -> Proof.context ->
+    term -> (string * typ) list -> (string * typ) list
   val add_free_names: Proof.context -> term -> string list -> string list
   val add_frees: Proof.context -> term -> (string * typ) list -> (string * typ) list
   val add_fixes_binding: binding list -> Proof.context -> string list * Proof.context
@@ -346,7 +348,7 @@
 (* specialized name space *)
 
 val is_fixed = Name_Space.defined_entry o fixes_space;
-fun newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer);
+fun is_newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer);
 
 val fixed_ord = Name_Space.entry_ord o fixes_space;
 val intern_fixed = Name_Space.intern o fixes_space;
@@ -383,6 +385,9 @@
 fun add_fixed ctxt =
   fold_aterms (fn Free (x, T) => is_fixed ctxt x ? insert (op =) (x, T) | _ => I);
 
+fun add_newly_fixed ctxt' ctxt =
+  fold_aterms (fn Free (x, T) => is_newly_fixed ctxt' ctxt x ? insert (op =) (x, T) | _ => I);
+
 
 (* declarations *)
 
@@ -474,7 +479,7 @@
 fun export_inst inner outer =
   let
     val declared_outer = is_declared outer;
-    val still_fixed = not o newly_fixed inner outer;
+    val still_fixed = not o is_newly_fixed inner outer;
 
     val gen_fixes =
       Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? cons y)