src/Pure/Isar/class_declaration.ML
changeset 38389 d7d915bae307
parent 38384 07c33be08476
child 38390 cb72d89bb444
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Thu Aug 12 13:23:46 2010 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Thu Aug 12 13:28:18 2010 +0200
     1.3 @@ -290,7 +290,7 @@
     1.4         Context.theory_map (Locale.add_registration (class, base_morph)
     1.5           (Option.map (rpair true) eq_morph) export_morph)
     1.6      #> Class.register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
     1.7 -    |> Named_Target.init (SOME class)
     1.8 +    |> Named_Target.init class
     1.9      |> pair class
    1.10    end;
    1.11  
    1.12 @@ -323,7 +323,7 @@
    1.13      fun after_qed some_wit =
    1.14        ProofContext.theory (Class.register_subclass (sub, sup)
    1.15          some_dep_morph some_wit export)
    1.16 -      #> ProofContext.theory_of #> Named_Target.init (SOME sub);
    1.17 +      #> ProofContext.theory_of #> Named_Target.init sub;
    1.18    in do_proof after_qed some_prop goal_ctxt end;
    1.19  
    1.20  fun user_proof after_qed some_prop =