src/HOL/Proofs/Lambda/WeakNorm.thy
changeset 40627 becf5d5187cc
parent 39157 b98909faaea8
child 41413 64cd30d6b0b8
     1.1 --- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -389,7 +389,7 @@
     1.4  ML {*
     1.5  fun dBtype_of_typ (Type ("fun", [T, U])) =
     1.6        @{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
     1.7 -  | dBtype_of_typ (TFree (s, _)) = (case explode s of
     1.8 +  | dBtype_of_typ (TFree (s, _)) = (case raw_explode s of
     1.9          ["'", a] => @{code Atom} (@{code nat} (ord a - 97))
    1.10        | _ => error "dBtype_of_typ: variable name")
    1.11    | dBtype_of_typ _ = error "dBtype_of_typ: bad type";
    1.12 @@ -458,7 +458,7 @@
    1.13  
    1.14  fun dBtype_of_typ (Type ("fun", [T, U])) =
    1.15        Norm.Fun (dBtype_of_typ T, dBtype_of_typ U)
    1.16 -  | dBtype_of_typ (TFree (s, _)) = (case explode s of
    1.17 +  | dBtype_of_typ (TFree (s, _)) = (case raw_explode s of
    1.18          ["'", a] => Norm.Atom (nat_of_int (ord a - 97))
    1.19        | _ => error "dBtype_of_typ: variable name")
    1.20    | dBtype_of_typ _ = error "dBtype_of_typ: bad type";