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/HOL/Typerep.thy
changeset 33384 1b5ba4e6a953
parent 31723 f5cafe803b55
child 33553 35f2b30593a8 
--- a/src/HOL/Typerep.thy	Mon Nov 02 20:30:40 2009 +0100
+++ b/src/HOL/Typerep.thy	Mon Nov 02 20:34:59 2009 +0100
@@ -29,7 +29,7 @@
     | typerep_tr' _ T ts = raise Match;
 in
   Sign.add_syntax_i
-    [("_TYPEREP", SimpleSyntax.read_typ "type => logic", Delimfix "(1TYPEREP/(1'(_')))")]
+    [("_TYPEREP", Simple_Syntax.read_typ "type => logic", Delimfix "(1TYPEREP/(1'(_')))")]
   #> Sign.add_trfuns ([], [("_TYPEREP", typerep_tr)], [], [])
   #> Sign.add_trfunsT [(@{const_syntax typerep}, typerep_tr')]
 end
isabelle