merged;

--- a/src/HOL/Statespace/StateSpaceEx.thy	Mon Nov 07 22:59:24 2011 +0100
+++ b/src/HOL/Statespace/StateSpaceEx.thy	Tue Nov 08 00:02:30 2011 +0100
@@ -476,4 +476,8 @@
 A987::nat A988::nat A989::nat A990::nat A991::nat A992::nat A993::nat
 A994::nat A995::nat A996::nat A997::nat A998::nat A999::nat A1000::nat
 
+lemma (in benchmark100) test: "s<A1 := a>\<cdot>A100 = s\<cdot>A100" by simp
+lemma (in benchmark500) test: "s<A1 := a>\<cdot>A100 = s\<cdot>A100" by simp
+lemma (in benchmark1000) test: "s<A1 := a>\<cdot>A100 = s\<cdot>A100" by simp
+
 end

--- a/src/Pure/term_subst.ML	Mon Nov 07 22:59:24 2011 +0100
+++ b/src/Pure/term_subst.ML	Tue Nov 08 00:02:30 2011 +0100
@@ -160,19 +160,26 @@
 
 (* zero var indexes *)
 
-fun zero_var_inst vars =
-  fold (fn v as ((x, i), X) => fn (inst, used) =>
-    let
-      val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used;
-    in if x = x' andalso i = 0 then (inst, used') else ((v, ((x', 0), X)) :: inst, used') end)
-  vars ([], Name.context) |> #1;
+structure TVars = Table(type key = indexname * sort val ord = Term_Ord.tvar_ord);
+structure Vars = Table(type key = indexname * typ val ord = Term_Ord.var_ord);
+
+fun zero_var_inst mk (v as ((x, i), X)) (inst, used) =
+  let
+    val (x', used') = Name.variant (if Name.is_bound x then "u" else x) used;
+  in if x = x' andalso i = 0 then (inst, used') else ((v, mk ((x', 0), X)) :: inst, used') end;
 
 fun zero_var_indexes_inst ts =
   let
-    val tvars = sort Term_Ord.tvar_ord (fold Term.add_tvars ts []);
-    val instT = map (apsnd TVar) (zero_var_inst tvars);
-    val vars = sort Term_Ord.var_ord (map (apsnd (instantiateT instT)) (fold Term.add_vars ts []));
-    val inst = map (apsnd Var) (zero_var_inst vars);
+    val (instT, _) =
+      TVars.fold (zero_var_inst TVar o #1)
+        ((fold o fold_types o fold_atyps) (fn TVar v =>
+          TVars.insert (K true) (v, ()) | _ => I) ts TVars.empty)
+        ([], Name.context);
+    val (inst, _) =
+      Vars.fold (zero_var_inst Var o #1)
+        ((fold o fold_aterms) (fn Var (xi, T) =>
+          Vars.insert (K true) ((xi, instantiateT instT T), ()) | _ => I) ts Vars.empty)
+        ([], Name.context);
   in (instT, inst) end;
 
 fun zero_var_indexes t = instantiate (zero_var_indexes_inst [t]) t;

--- a/src/Pure/variable.ML	Mon Nov 07 22:59:24 2011 +0100
+++ b/src/Pure/variable.ML	Tue Nov 08 00:02:30 2011 +0100
@@ -403,11 +403,11 @@
 fun export_inst inner outer =
   let
     val declared_outer = is_declared outer;
+    fun still_fixed x = is_fixed outer x orelse not (is_fixed inner x);
 
     val gen_fixes =
       Symtab.fold (fn (y, _) => not (is_fixed outer y) ? cons y)
         (#2 (fixes_of inner)) [];
-    val still_fixed = not o member (op =) gen_fixes;
 
     val type_occs_inner = type_occs_of inner;
     fun gen_fixesT ts =