src/HOL/Tools/datatype_realizer.ML
changeset 22578 b0eb5652f210
parent 21646 c07b5b0e8492
child 22596 d0d2af4db18f
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Wed Apr 04 00:10:59 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Wed Apr 04 00:11:03 2007 +0200
     1.3 @@ -42,7 +42,6 @@
     1.4  
     1.5  fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : datatype_info) (is, thy) =
     1.6    let
     1.7 -    val sg = sign_of thy;
     1.8      val recTs = get_rec_types descr sorts;
     1.9      val pnames = if length descr = 1 then ["P"]
    1.10        else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
    1.11 @@ -115,7 +114,7 @@
    1.12        (map (fn ((((i, _), T), U), tname) =>
    1.13          make_pred i U T (mk_proj i is r) (Free (tname, T)))
    1.14            (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
    1.15 -    val cert = cterm_of sg;
    1.16 +    val cert = cterm_of thy;
    1.17      val inst = map (pairself cert) (map head_of (HOLogic.dest_conj
    1.18        (HOLogic.dest_Trueprop (concl_of induction))) ~~ ps);
    1.19