src/Pure/Isar/isar_syn.ML
changeset 20365 5fad57dfd7c9
parent 20305 16c8f44b1852
child 20574 a10885a269cb
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Aug 09 00:12:35 2006 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 09 00:12:37 2006 +0200
     1.3 @@ -360,16 +360,16 @@
     1.4    OuterSyntax.command "interpretation"
     1.5      "prove and register interpretation of locale expression in theory or locale" K.thy_goal
     1.6      (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! P.locale_expr
     1.7 -      >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale)) ||
     1.8 -     P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts >> (fn ((x, y), z) =>
     1.9 -      Toplevel.print o Toplevel.theory_to_proof (Locale.interpretation x y z)));
    1.10 +      >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) ||
    1.11 +      P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts >> (fn ((x, y), z) =>
    1.12 +        Toplevel.print o Toplevel.theory_to_proof (Locale.interpretation I x y z)));
    1.13  
    1.14  val interpretP =
    1.15    OuterSyntax.command "interpret"
    1.16      "prove and register interpretation of locale expression in proof context"
    1.17      (K.tag_proof K.prf_goal)
    1.18      (P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts >> (fn ((x, y), z) =>
    1.19 -      Toplevel.print o Toplevel.proof' (Locale.interpret x y z)));
    1.20 +      Toplevel.print o Toplevel.proof' (Locale.interpret Seq.single x y z)));
    1.21  
    1.22  
    1.23