1.1 --- a/src/HOL/Typerep.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Typerep.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  (* Author: Florian Haftmann, TU Muenchen *)
     1.5  
     1.6 -section {* Reflecting Pure types into HOL *}
     1.7 +section \<open>Reflecting Pure types into HOL\<close>
     1.8  
     1.9  theory Typerep
    1.10  imports String
    1.11 @@ -20,7 +20,7 @@
    1.12  syntax
    1.13    "_TYPEREP" :: "type => logic"  ("(1TYPEREP/(1'(_')))")
    1.14  
    1.15 -parse_translation {*
    1.16 +parse_translation \<open>
    1.17    let
    1.18      fun typerep_tr (*"_TYPEREP"*) [ty] =
    1.19            Syntax.const @{const_syntax typerep} $
    1.20 @@ -28,9 +28,9 @@
    1.21                (Syntax.const @{type_syntax itself} $ ty))
    1.22        | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts);
    1.23    in [(@{syntax_const "_TYPEREP"}, K typerep_tr)] end
    1.24 -*}
    1.25 +\<close>
    1.26  
    1.27 -typed_print_translation {*
    1.28 +typed_print_translation \<open>
    1.29    let
    1.30      fun typerep_tr' ctxt (*"typerep"*)
    1.31              (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _]))
    1.32 @@ -39,9 +39,9 @@
    1.33              (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ ctxt T, ts)
    1.34        | typerep_tr' _ T ts = raise Match;
    1.35    in [(@{const_syntax typerep}, typerep_tr')] end
    1.36 -*}
    1.37 +\<close>
    1.38  
    1.39 -setup {*
    1.40 +setup \<open>
    1.41  let
    1.42  
    1.43  fun add_typerep tyco thy =
    1.44 @@ -76,7 +76,7 @@
    1.45  #> Code.abstype_interpretation (ensure_typerep o fst)
    1.46  
    1.47  end
    1.48 -*}
    1.49 +\<close>
    1.50  
    1.51  lemma [code]:
    1.52    "HOL.equal (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> HOL.equal tyco1 tyco2