tuned;

--- a/src/Pure/Isar/element.ML	Mon Jun 12 21:19:05 2006 +0200
+++ b/src/Pure/Isar/element.ML	Mon Jun 12 21:19:06 2006 +0200
@@ -310,7 +310,7 @@
 
 fun hyps_rule rule th =
   let
-    val cterm_rule = Thm.reflexive #> rule #> Thm.cprop_of #> Drule.dest_equals #> #1;
+    val cterm_rule = Drule.mk_term #> rule #> Drule.dest_term;
     val {hyps, ...} = Thm.crep_thm th;
   in
     Drule.implies_elim_list

--- a/src/Pure/unify.ML	Mon Jun 12 21:19:05 2006 +0200
+++ b/src/Pure/unify.ML	Mon Jun 12 21:19:06 2006 +0200
@@ -650,11 +650,11 @@
           in ((x, i - offset), (decr_indexesT T', decr_indexes t')) end;
 
         fun result env =
-          (warning "FIXME"; if Envir.above env maxidx then
+          if Envir.above env maxidx then
             SOME (Envir.Envir {maxidx = maxidx,
-              iTs = Vartab.make (map (PolyML.print o (norm_tvar env)) pat_tvars),
-              asol = Vartab.make (map (PolyML.print o (norm_var env)) pat_vars)})
-          else NONE);
+              iTs = Vartab.make (map (norm_tvar env) pat_tvars),
+              asol = Vartab.make (map (norm_var env) pat_vars)})
+          else NONE;
 
         val empty = Envir.empty maxidx';
       in