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/old_locale.ML
changeset 29383 223f18cfbb32
parent 29360 a5be60c3674e 
--- a/src/Pure/Isar/old_locale.ML	Wed Jan 07 12:10:22 2009 +0100
+++ b/src/Pure/Isar/old_locale.ML	Wed Jan 07 16:22:10 2009 +0100
@@ -116,7 +116,7 @@
     theory -> Proof.state
   val interpretation_in_locale: (Proof.context -> Proof.context) ->
     xstring * expr -> theory -> Proof.state
-  val interpret: (Proof.state -> Proof.state Seq.seq) ->
+  val interpret: (Proof.state -> Proof.state) ->
     (Binding.T -> Binding.T) -> expr ->
     term option list * (Attrib.binding * term) list ->
     bool -> Proof.state ->
@@ -2478,7 +2478,7 @@
 
 val interpret = gen_interpret prep_local_registration;
 fun interpret_cmd interp_prfx = snd oooo gen_interpret prep_local_registration_cmd
-  Seq.single (standard_name_morph interp_prfx);
+  I (standard_name_morph interp_prfx);
 
 end;
isabelle