src/Pure/Isar/expression.ML
changeset 32805 9b535493ac8d
parent 32804 ca430e6aee1c
parent 32512 d14762642cdd
child 32807 c4f03b0cb753
child 32845 d2d0b9b1a69d
     1.1 --- a/src/Pure/Isar/expression.ML	Tue Sep 29 22:15:54 2009 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Oct 01 07:40:25 2009 +0200
     1.3 @@ -840,7 +840,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