Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/isar_syn.ML
changeset 28259 5b2af04ec9fb
parent 28114 2637fb838f74
child 28269 b1e5e6c4c10e 
--- a/src/Pure/Isar/isar_syn.ML	Wed Sep 17 11:42:25 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Sep 17 15:21:30 2008 +0200
@@ -400,7 +400,7 @@
       opt_prefix  -- SpecParse.locale_expr -- SpecParse.locale_insts
         >> (fn ((name, expr), insts) => Toplevel.print o
             Toplevel.theory_to_proof
-              (Locale.interpretation I (true, Name.name_of name) expr insts)));
+              (Locale.interpretation I (true, Name.name_of name) expr insts #> snd)));
 
 val _ =
   OuterSyntax.command "interpret"
@@ -409,7 +409,7 @@
     (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
       >> (fn ((name, expr), insts) => Toplevel.print o
           Toplevel.proof'
-            (Locale.interpret Seq.single (true, Name.name_of name) expr insts)));
+            (fn int => Locale.interpret Seq.single (true, Name.name_of name) expr insts int #> snd)));
 
 
 (* classes *)
isabelle