src/Pure/Isar/class_target.ML
changeset 35021 c839a4c670c6
parent 33969 1e7ca47c6c3d
child 35126 ce6544f42eb9
     1.1 --- a/src/Pure/Isar/class_target.ML	Sun Feb 07 19:31:55 2010 +0100
     1.2 +++ b/src/Pure/Isar/class_target.ML	Sun Feb 07 19:33:34 2010 +0100
     1.3 @@ -233,7 +233,7 @@
     1.4  fun register_subclass (sub, sup) some_dep_morph some_wit export thy =
     1.5    let
     1.6      val intros = (snd o rules thy) sup :: map_filter I
     1.7 -      [Option.map (Drule.standard' o Element.conclude_witness) some_wit,
     1.8 +      [Option.map (Drule.export_without_context_open o Element.conclude_witness) some_wit,
     1.9          (fst o rules thy) sub];
    1.10      val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
    1.11      val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))