src/Pure/Isar/expression.ML
changeset 38350 480b2de9927c
parent 38316 88e774d09fbc
child 38389 d7d915bae307
     1.1 --- a/src/Pure/Isar/expression.ML	Wed Aug 11 14:41:16 2010 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed Aug 11 14:45:38 2010 +0200
     1.3 @@ -775,7 +775,7 @@
     1.4      val loc_ctxt = thy'
     1.5        |> Locale.register_locale binding (extraTs, params)
     1.6            (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps')
     1.7 -      |> Theory_Target.init (SOME name)
     1.8 +      |> Named_Target.init (SOME name)
     1.9        |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
    1.10  
    1.11    in (name, loc_ctxt) end;
    1.12 @@ -870,7 +870,7 @@
    1.13  fun gen_sublocale prep_expr intern raw_target expression thy =
    1.14    let
    1.15      val target = intern thy raw_target;
    1.16 -    val target_ctxt = Theory_Target.init (SOME target) thy;
    1.17 +    val target_ctxt = Named_Target.init (SOME target) thy;
    1.18      val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
    1.19      fun after_qed witss = ProofContext.theory
    1.20        (fold (fn ((dep, morph), wits) => Locale.add_dependency