locale interpretation command: after_qed;
authorwenzelm
Wed Aug 09 00:12:37 2006 +0200 (2006-08-09 ago)
changeset 203655fad57dfd7c9
parent 20364 f7e440f2eb2f
child 20366 867696dc64fc
locale interpretation command: after_qed;
src/Pure/Isar/isar_syn.ML
     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