src/Pure/Isar/class.ML
changeset 38350 480b2de9927c
parent 38107 3a46cebd7983
child 38352 4c8bcb826e83
     1.1 --- a/src/Pure/Isar/class.ML	Wed Aug 11 14:41:16 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Wed Aug 11 14:45:38 2010 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  signature CLASS =
     1.5  sig
     1.6    include CLASS_TARGET
     1.7 -    (*FIXME the split into class_target.ML, theory_target.ML and
     1.8 +    (*FIXME the split into class_target.ML, Named_Target.ML and
     1.9        class.ML is artificial*)
    1.10  
    1.11    val class: binding -> class list -> Element.context_i list
    1.12 @@ -296,7 +296,7 @@
    1.13         Context.theory_map (Locale.add_registration (class, base_morph)
    1.14           (Option.map (rpair true) eq_morph) export_morph)
    1.15      #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
    1.16 -    |> Theory_Target.init (SOME class)
    1.17 +    |> Named_Target.init (SOME class)
    1.18      |> pair class
    1.19    end;
    1.20  
    1.21 @@ -316,7 +316,7 @@
    1.22    let
    1.23      val thy = ProofContext.theory_of lthy;
    1.24      val proto_sup = prep_class thy raw_sup;
    1.25 -    val proto_sub = case Theory_Target.peek lthy
    1.26 +    val proto_sub = case Named_Target.peek lthy
    1.27       of {is_class = false, ...} => error "Not in a class context"
    1.28        | {target, ...} => target;
    1.29      val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
    1.30 @@ -329,7 +329,7 @@
    1.31      fun after_qed some_wit =
    1.32        ProofContext.theory (register_subclass (sub, sup)
    1.33          some_dep_morph some_wit export)
    1.34 -      #> ProofContext.theory_of #> Theory_Target.init (SOME sub);
    1.35 +      #> ProofContext.theory_of #> Named_Target.init (SOME sub);
    1.36    in do_proof after_qed some_prop goal_ctxt end;
    1.37  
    1.38  fun user_proof after_qed some_prop =