src/HOL/Nominal/nominal_primrec.ML
changeset 22692 1e057a3f087d
parent 22434 081a62852313
child 22709 9ab51bac6287
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sun Apr 15 14:31:47 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Apr 15 14:31:49 2007 +0200
     1.3 @@ -206,10 +206,11 @@
     1.4      val frees = ls @ x :: rs;
     1.5      val rhs = list_abs_free (frees,
     1.6        list_comb (Const (rec_name, dummyT), fs @ [Free x]))
     1.7 -    val defpair = (Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def",
     1.8 -                   Logic.mk_equals (Const (fname, dummyT), rhs));
     1.9 -    val defpair' as (_, _ $ _ $ t) = Theory.inferT_axm thy defpair
    1.10 -  in (defpair', subst_bounds (rev (map Free frees), strip_abs_body t)) end;
    1.11 +    val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def";
    1.12 +    val def_prop as _ $ _ $ t =
    1.13 +      singleton (ProofContext.infer_types (ProofContext.init thy))
    1.14 +        (Logic.mk_equals (Const (fname, dummyT), rhs), propT) |> #1;
    1.15 +  in ((def_name, def_prop), subst_bounds (rev (map Free frees), strip_abs_body t)) end;
    1.16  
    1.17  
    1.18  (* find datatypes which contain all datatypes in tnames' *)