src/Pure/Isar/expression.ML
changeset 32512 d14762642cdd
parent 32074 76d6ba08a05f
child 32785 ec5292653aff
child 32805 9b535493ac8d
     1.1 --- a/src/Pure/Isar/expression.ML	Wed Sep 02 14:11:45 2009 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Sep 03 15:39:02 2009 +0200
     1.3 @@ -839,7 +839,7 @@
     1.4  fun gen_sublocale prep_expr intern raw_target expression thy =
     1.5    let
     1.6      val target = intern thy raw_target;
     1.7 -    val target_ctxt = Locale.init target thy;
     1.8 +    val target_ctxt = TheoryTarget.init (SOME target) thy;
     1.9      val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
    1.10      fun after_qed witss = ProofContext.theory
    1.11        (fold (fn ((dep, morph), wits) => Locale.add_dependency