src/Pure/Isar/class.ML
changeset 31794 71af1fd6a5e4
parent 31696 8b3dac635907
child 31904 a86896359ca4
     1.1 --- a/src/Pure/Isar/class.ML	Wed Jun 24 20:52:49 2009 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Jun 24 21:28:02 2009 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4      (* assm_intro *)
     1.5      fun prove_assm_intro thm =
     1.6        let
     1.7 -        val ((_, [thm']), _) = Variable.import_thms true [thm] empty_ctxt;
     1.8 +        val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
     1.9          val thm'' = Morphism.thm (const_morph $> eq_morph) thm';
    1.10          val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
    1.11        in SkipProof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;