tuned;
authorwenzelm
Mon Jun 12 21:19:06 2006 +0200 (2006-06-12)
changeset 19866d47f32a4964a
parent 19865 8e1cee9e03dc
child 19867 474cc9b49239
tuned;
src/Pure/Isar/element.ML
src/Pure/unify.ML
     1.1 --- a/src/Pure/Isar/element.ML	Mon Jun 12 21:19:05 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Mon Jun 12 21:19:06 2006 +0200
     1.3 @@ -310,7 +310,7 @@
     1.4  
     1.5  fun hyps_rule rule th =
     1.6    let
     1.7 -    val cterm_rule = Thm.reflexive #> rule #> Thm.cprop_of #> Drule.dest_equals #> #1;
     1.8 +    val cterm_rule = Drule.mk_term #> rule #> Drule.dest_term;
     1.9      val {hyps, ...} = Thm.crep_thm th;
    1.10    in
    1.11      Drule.implies_elim_list
     2.1 --- a/src/Pure/unify.ML	Mon Jun 12 21:19:05 2006 +0200
     2.2 +++ b/src/Pure/unify.ML	Mon Jun 12 21:19:06 2006 +0200
     2.3 @@ -650,11 +650,11 @@
     2.4            in ((x, i - offset), (decr_indexesT T', decr_indexes t')) end;
     2.5  
     2.6          fun result env =
     2.7 -          (warning "FIXME"; if Envir.above env maxidx then
     2.8 +          if Envir.above env maxidx then
     2.9              SOME (Envir.Envir {maxidx = maxidx,
    2.10 -              iTs = Vartab.make (map (PolyML.print o (norm_tvar env)) pat_tvars),
    2.11 -              asol = Vartab.make (map (PolyML.print o (norm_var env)) pat_vars)})
    2.12 -          else NONE);
    2.13 +              iTs = Vartab.make (map (norm_tvar env) pat_tvars),
    2.14 +              asol = Vartab.make (map (norm_var env) pat_vars)})
    2.15 +          else NONE;
    2.16  
    2.17          val empty = Envir.empty maxidx';
    2.18        in