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