src/HOL/Tools/Datatype/datatype_realizer.ML
changeset 56254 a2dd9200854d
parent 54895 515630483010
child 58111 82db9ad610b9
     1.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Mar 22 18:16:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sat Mar 22 18:19:57 2014 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4        else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
     1.5  
     1.6      val rec_result_Ts = map (fn ((i, _), P) =>
     1.7 -        if member (op =) is i then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT)
     1.8 +        if member (op =) is i then TFree ("'" ^ P, @{sort type}) else HOLogic.unitT)
     1.9        (descr ~~ pnames);
    1.10  
    1.11      fun make_pred i T U r x =
    1.12 @@ -163,8 +163,8 @@
    1.13    let
    1.14      val ctxt = Proof_Context.init_global thy;
    1.15      val cert = cterm_of thy;
    1.16 -    val rT = TFree ("'P", HOLogic.typeS);
    1.17 -    val rT' = TVar (("'P", 0), HOLogic.typeS);
    1.18 +    val rT = TFree ("'P", @{sort type});
    1.19 +    val rT' = TVar (("'P", 0), @{sort type});
    1.20  
    1.21      fun make_casedist_prem T (cname, cargs) =
    1.22        let