src/Pure/Isar/element.ML
changeset 20218 be3bfb0699ba
parent 20150 baa589c574ff
child 20233 ece639738db3
     1.1 --- a/src/Pure/Isar/element.ML	Wed Jul 26 19:23:04 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Wed Jul 26 19:37:41 2006 +0200
     1.3 @@ -219,7 +219,7 @@
     1.4      val ((xs, prop'), ctxt') = Variable.focus prop ctxt;
     1.5      val As = Logic.strip_imp_prems (Thm.term_of prop');
     1.6      fun var (x, T) = (ProofContext.revert_skolem ctxt' x, SOME T);
     1.7 -  in (("", (map var xs, As)), ctxt') end;
     1.8 +  in (("", (map (var o Term.dest_Free o Thm.term_of) xs, As)), ctxt') end;
     1.9  
    1.10  in
    1.11  
    1.12 @@ -231,7 +231,7 @@
    1.13      val th = Goal.norm_hhf raw_th;
    1.14      val is_elim = ObjectLogic.is_elim th;
    1.15  
    1.16 -    val ([th'], ctxt') = Variable.import true [th] ctxt;
    1.17 +    val ((_, [th']), ctxt') = Variable.import true [th] ctxt;
    1.18      val prop = Thm.prop_of th';
    1.19      val (prems, concl) = Logic.strip_horn prop;
    1.20      val concl_term = ObjectLogic.drop_judgment thy concl;