src/HOL/Tools/datatype_package.ML
changeset 12338 de0f4a63baa5
parent 12311 ce5f9e61c037
child 12448 473cb9f9e237
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Sat Dec 01 18:51:46 2001 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Dec 01 18:52:32 2001 +0100
     1.3 @@ -365,7 +365,7 @@
     1.4     | _ => None)
     1.5    | distinct_proc sg _ _ = None;
     1.6  
     1.7 -val distinct_pats = [Thm.read_cterm (Theory.sign_of HOL.thy) ("s = t", HOLogic.termT)];
     1.8 +val distinct_pats = [HOLogic.read_cterm (Theory.sign_of HOL.thy) "s = t"];
     1.9  val distinct_simproc = mk_simproc distinctN distinct_pats distinct_proc;
    1.10  
    1.11  val dist_ss = HOL_ss addsimprocs [distinct_simproc];
    1.12 @@ -460,7 +460,7 @@
    1.13            (constrs ~~ constr_syntax')) ((hd descr) ~~ newTs ~~ constr_syntax);
    1.14  
    1.15      val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
    1.16 -      replicate (length descr') HOLogic.termS);
    1.17 +      replicate (length descr') HOLogic.typeS);
    1.18  
    1.19      val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
    1.20        map (fn (_, cargs) =>
    1.21 @@ -484,7 +484,7 @@
    1.22      val size_names = DatatypeProp.indexify_names
    1.23        (map (fn T => name_of_typ T ^ "_size") (drop (length (hd descr), recTs)));
    1.24  
    1.25 -    val freeT = TFree (variant used "'t", HOLogic.termS);
    1.26 +    val freeT = TFree (variant used "'t", HOLogic.typeS);
    1.27      val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
    1.28        map (fn (_, cargs) =>
    1.29          let val Ts = map (typ_of_dtyp descr' sorts) cargs