src/HOL/Typerep.thy
changeset 35115 446c5063e4fd
parent 33553 35f2b30593a8
child 35299 4f4d5bf4ea08
--- a/src/HOL/Typerep.thy	Thu Feb 11 22:55:16 2010 +0100
+++ b/src/HOL/Typerep.thy	Thu Feb 11 23:00:22 2010 +0100
@@ -17,22 +17,27 @@
 
 end
 
-setup {*
+syntax
+  "_TYPEREP" :: "type => logic"  ("(1TYPEREP/(1'(_')))")
+
+parse_translation {*
 let
   fun typerep_tr (*"_TYPEREP"*) [ty] =
-        Lexicon.const @{const_syntax typerep} $ (Lexicon.const "_constrain" $ Lexicon.const "TYPE" $
-          (Lexicon.const "itself" $ ty))
+        Syntax.const @{const_syntax typerep} $
+          (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $
+            (Syntax.const "itself" $ ty))  (* FIXME @{type_syntax} *)
     | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
-  fun typerep_tr' show_sorts (*"typerep"*)
+in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end
+*}
+
+typed_print_translation {*
+let
+  fun typerep_tr' show_sorts (*"typerep"*)  (* FIXME @{type_syntax} *)
           (Type ("fun", [Type ("itself", [T]), _])) (Const (@{const_syntax TYPE}, _) :: ts) =
-        Term.list_comb (Lexicon.const "_TYPEREP" $ Syntax.term_of_typ show_sorts T, ts)
+        Term.list_comb
+          (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax.term_of_typ show_sorts T, ts)
     | typerep_tr' _ T ts = raise Match;
-in
-  Sign.add_syntax_i
-    [("_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
+in [(@{const_syntax typerep}, typerep_tr')] end
 *}
 
 setup {*