src/HOL/Tools/primrec_package.ML
changeset 5891 92e0f5e6fd17
parent 5719 2aed60cdb9f2
child 6032 c4e62bab69bd
     1.1 --- a/src/HOL/Tools/primrec_package.ML	Mon Nov 16 11:13:28 1998 +0100
     1.2 +++ b/src/HOL/Tools/primrec_package.ML	Mon Nov 16 11:14:02 1998 +0100
     1.3 @@ -225,7 +225,7 @@
     1.4        commas names1 ^ " ...");
     1.5      val char_thms = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (sign_of thy') t)
     1.6          (fn _ => [rtac refl 1])) eqns;
     1.7 -    val tsimps = map Attribute.tthm_of char_thms;
     1.8 +    val tsimps = Attribute.tthms_of char_thms;
     1.9      val thy'' = thy' |>
    1.10        PureThy.add_tthmss [(("simps", tsimps), [Simplifier.simp_add_global])] |>
    1.11        PureThy.add_tthms (map (rpair [])