tuned;

--- a/src/HOL/OrderedGroup.thy	Tue Jun 06 20:42:27 2006 +0200
+++ b/src/HOL/OrderedGroup.thy	Tue Jun 06 20:42:28 2006 +0200
@@ -8,7 +8,7 @@
 
 theory OrderedGroup
 imports Inductive LOrder
-uses "../Provers/Arith/abel_cancel.ML"
+uses "~~/src/Provers/Arith/abel_cancel.ML"
 begin
 
 text {*

--- a/src/HOL/Tools/rewrite_hol_proof.ML	Tue Jun 06 20:42:27 2006 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Tue Jun 06 20:42:28 2006 +0200
@@ -103,7 +103,7 @@
  \  (allI % TYPE('a) % P %%  \
  \    (Lam x.  \
  \        iffD2 % P x % Q x %% (prf % x) %%  \
- \         (spec % TYPE('a) % ?Q % x %% prf')))",
+ \         (spec % TYPE('a) % Q % x %% prf')))",
 
    (* Ex *)
 

--- a/src/Provers/Arith/abel_cancel.ML	Tue Jun 06 20:42:27 2006 +0200
+++ b/src/Provers/Arith/abel_cancel.ML	Tue Jun 06 20:42:28 2006 +0200
@@ -118,7 +118,7 @@
    handle Cancel => NONE;
 
  val rel_conv =
-     Simplifier.simproc_i (Theory.deref thy_ref) "cancel_relations"
-       (map Data.dest_eqI eqI_rules) rel_proc;
+     Simplifier.mk_simproc "cancel_relations"
+       (map (Thm.cterm_of (Theory.deref thy_ref) o Data.dest_eqI) eqI_rules) rel_proc;
 
 end;

--- a/src/Pure/Isar/attrib.ML	Tue Jun 06 20:42:27 2006 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue Jun 06 20:42:28 2006 +0200
@@ -244,10 +244,10 @@
 
 in
 
-fun read_instantiate mixed_insts (generic, thm) =
+fun read_instantiate mixed_insts (context, thm) =
   let
-    val thy = Context.theory_of generic;
-    val ctxt = Context.proof_of generic;
+    val thy = Context.theory_of context;
+    val ctxt = Context.proof_of context;
 
     val (type_insts, term_insts) = List.partition (is_tvar o fst) (map snd mixed_insts);
     val internal_insts = term_insts |> map_filter
@@ -316,7 +316,7 @@
         else
           Args.assign (SOME (Args.Term (the (AList.lookup (op =) term_insts''' xi)))) arg);
 
-  in (generic, thm''' |> RuleCases.save thm) end;
+  in (context, thm''' |> RuleCases.save thm) end;
 
 end;
 
@@ -344,7 +344,7 @@
 
 local
 
-fun read_instantiate' (args, concl_args) (generic, thm) =
+fun read_instantiate' (args, concl_args) (context, thm) =
   let
     fun zip_vars _ [] = []
       | zip_vars (_ :: xs) ((_, NONE) :: rest) = zip_vars xs rest
@@ -353,7 +353,7 @@
     val insts =
       zip_vars (Drule.vars_of_terms [Thm.prop_of thm]) args @
       zip_vars (Drule.vars_of_terms [Thm.concl_of thm]) concl_args;
-  in read_instantiate insts (generic, thm) end;
+  in read_instantiate insts (context, thm) end;
 
 val value =
   Args.internal_term >> Args.Term ||

--- a/src/Pure/meta_simplifier.ML	Tue Jun 06 20:42:27 2006 +0200
+++ b/src/Pure/meta_simplifier.ML	Tue Jun 06 20:42:28 2006 +0200
@@ -332,6 +332,7 @@
       Proc {name = name, lhs = lhs, proc = proc, id = id}))
   end;
 
+(* FIXME avoid global thy and Logic.varify *)
 fun simproc_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify);
 fun simproc thy name = simproc_i thy name o map (Sign.read_term thy);