tuned;

--- a/src/Pure/Proof/proofchecker.ML	Fri Jul 15 15:44:15 2005 +0200
+++ b/src/Pure/Proof/proofchecker.ML	Fri Jul 15 15:44:17 2005 +0200
@@ -19,7 +19,7 @@
 (***** construct a theorem out of a proof term *****)
 
 fun lookup_thm thy =
-  let val tab = foldr Symtab.update Symtab.empty (PureThy.all_thms_of thy)
+  let val tab = fold_rev (curry Symtab.update) (PureThy.all_thms_of thy) Symtab.empty
   in
     (fn s => case Symtab.lookup (tab, s) of
        NONE => error ("Unknown theorem " ^ quote s)
@@ -37,7 +37,7 @@
 
     fun thm_of_atom thm Ts =
       let
-        val tvars = term_tvars (prop_of thm);
+        val tvars = term_tvars (Thm.full_prop_of thm);
         val (thm', fmap) = Thm.varifyT' [] thm;
         val ctye = map (pairself (Thm.ctyp_of sg))
           (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)

--- a/src/Pure/Proof/reconstruct.ML	Fri Jul 15 15:44:15 2005 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Fri Jul 15 15:44:17 2005 +0200
@@ -8,10 +8,10 @@
 signature RECONSTRUCT =
 sig
   val quiet_mode : bool ref
-  val reconstruct_proof : Sign.sg -> term -> Proofterm.proof -> Proofterm.proof
+  val reconstruct_proof : theory -> term -> Proofterm.proof -> Proofterm.proof
   val prop_of' : term list -> Proofterm.proof -> term
   val prop_of : Proofterm.proof -> term
-  val expand_proof : Sign.sg -> (string * term option) list ->
+  val expand_proof : theory -> (string * term option) list ->
     Proofterm.proof -> Proofterm.proof
 end;
 
@@ -24,7 +24,7 @@
 fun message s = if !quiet_mode then () else writeln s;
 
 fun vars_of t = rev (fold_aterms
-  (fn v as Var _ => (fn vs => v ins vs) | _ => I) t []);
+  (fn v as Var _ => insert (op =) v | _ => I) t []);
 
 fun forall_intr (t, prop) =
   let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
@@ -232,12 +232,7 @@
       | mk_cnstrts _ _ _ _ _ = error "reconstruct_proof: minimal proof object"
   in mk_cnstrts env [] [] Symtab.empty cprf end;
 
-fun add_term_ixns (is, Var (i, T)) = add_typ_ixns (i ins is, T)
-  | add_term_ixns (is, Free (_, T)) = add_typ_ixns (is, T)
-  | add_term_ixns (is, Const (_, T)) = add_typ_ixns (is, T)
-  | add_term_ixns (is, t1 $ t2) = add_term_ixns (add_term_ixns (is, t1), t2)
-  | add_term_ixns (is, Abs (_, T, t)) = add_term_ixns (add_typ_ixns (is, T), t)
-  | add_term_ixns (is, _) = is;
+fun add_term_ixns (is, t) = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I) t is;
 
 
 (**** update list of free variables of constraints ****)
@@ -361,7 +356,8 @@
           let
             fun inc i =
               map_proof_terms (Logic.incr_indexes ([], i)) (incr_tvar i);
-            val (maxidx', prf, prfs') = (case assoc (prfs, (a, prop)) of
+            val (maxidx', prf, prfs') =
+              (case gen_assoc (op =) (prfs, (a, prop)) of
                 NONE =>
                   let
                     val _ = message ("Reconstructing proof of " ^ a);

--- a/src/Pure/logic.ML	Fri Jul 15 15:44:15 2005 +0200
+++ b/src/Pure/logic.ML	Fri Jul 15 15:44:17 2005 +0200
@@ -331,26 +331,27 @@
 
 (*Converts Frees to Vars and TFrees to TVars so that axioms can be written
   without (?) everywhere*)
-fun varify (Const(a,T)) = Const(a, Type.varifyT T)
-  | varify (Free(a,T)) = Var((a,0), Type.varifyT T)
-  | varify (Var(ixn,T)) = Var(ixn, Type.varifyT T)
-  | varify (Abs (a,T,body)) = Abs (a, Type.varifyT T, varify body)
-  | varify (f$t) = varify f $ varify t
-  | varify t = t;
+fun varify (Const(a, T)) = Const (a, Type.varifyT T)
+  | varify (Free (a, T)) = Var ((a, 0), Type.varifyT T)
+  | varify (Var (ixn, T)) = Var (ixn, Type.varifyT T)
+  | varify (t as Bound _) = t
+  | varify (Abs (a, T, body)) = Abs (a, Type.varifyT T, varify body)
+  | varify (f $ t) = varify f $ varify t;
 
 (*Inverse of varify.  Converts axioms back to their original form.*)
-fun unvarify (Const(a,T))    = Const(a, Type.unvarifyT T)
-  | unvarify (Free(a,T))     = Free(a, Type.unvarifyT T)  (* CB: added *)
-  | unvarify (Var((a,0), T)) = Free(a, Type.unvarifyT T)
-  | unvarify (Var(ixn,T))    = Var(ixn, Type.unvarifyT T)  (*non-0 index!*)
-  | unvarify (Abs (a,T,body)) = Abs (a, Type.unvarifyT T, unvarify body)
-  | unvarify (f$t) = unvarify f $ unvarify t
-  | unvarify t = t;
+fun unvarify (Const (a, T)) = Const (a, Type.unvarifyT T)
+  | unvarify (Free (a, T)) = Free (a, Type.unvarifyT T)
+  | unvarify (Var ((a, 0), T)) = Free (a, Type.unvarifyT T)
+  | unvarify (Var (ixn, T)) = Var (ixn, Type.unvarifyT T)  (*non-0 index!*)
+  | unvarify (t as Bound _) = t
+  | unvarify (Abs (a, T, body)) = Abs (a, Type.unvarifyT T, unvarify body)
+  | unvarify (f $ t) = unvarify f $ unvarify t;
 
 
-(*Get subgoal i*)
-fun get_goal st i = List.nth (strip_imp_prems st, i-1)
-  handle Subscript => error "Goal number out of range";
+(* goal states *)
+
+fun get_goal st i = nth_prem (i, st)
+  handle TERM _ => error "Goal number out of range";
 
 (*reverses parameters for substitution*)
 fun goal_params st i =