# HG changeset patch
# User wenzelm
# Date 1150139946 -7200
# Node ID d47f32a4964af013fa23344d9edfdc40dfdf423b
# Parent  8e1cee9e03dc337cc9b97500f1f32148569b3d4c
tuned;

diff -r 8e1cee9e03dc -r d47f32a4964a src/Pure/Isar/element.ML
--- 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
diff -r 8e1cee9e03dc -r d47f32a4964a src/Pure/unify.ML
--- 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