src/Pure/Isar/class.ML
changeset 33553 35f2b30593a8
parent 33173 b8ca12f6681a
child 33671 4b0f2599ed48
     1.1 --- a/src/Pure/Isar/class.ML	Tue Nov 10 15:33:35 2009 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Tue Nov 10 16:04:57 2009 +0100
     1.3 @@ -290,7 +290,7 @@
     1.4         Locale.add_registration (class, base_morph $> eq_morph) NONE export_morph
     1.5           (*FIXME should not modify base_morph, although admissible*)
     1.6      #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
     1.7 -    |> TheoryTarget.init (SOME class)
     1.8 +    |> Theory_Target.init (SOME class)
     1.9      |> pair class
    1.10    end;
    1.11  
    1.12 @@ -310,7 +310,7 @@
    1.13    let
    1.14      val thy = ProofContext.theory_of lthy;
    1.15      val proto_sup = prep_class thy raw_sup;
    1.16 -    val proto_sub = case TheoryTarget.peek lthy
    1.17 +    val proto_sub = case Theory_Target.peek lthy
    1.18       of {is_class = false, ...} => error "Not in a class context"
    1.19        | {target, ...} => target;
    1.20      val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
    1.21 @@ -323,7 +323,7 @@
    1.22      fun after_qed some_wit =
    1.23        ProofContext.theory (register_subclass (sub, sup)
    1.24          some_dep_morph some_wit export)
    1.25 -      #> ProofContext.theory_of #> TheoryTarget.init (SOME sub);
    1.26 +      #> ProofContext.theory_of #> Theory_Target.init (SOME sub);
    1.27    in do_proof after_qed some_prop goal_ctxt end;
    1.28  
    1.29  fun user_proof after_qed some_prop =