changeset 9315 | f793f05024f6 |
parent 9298 | 7d9b562a750b |
child 9405 | 3235873fdd90 |
--- a/src/HOL/Tools/inductive_package.ML Thu Jul 13 23:11:38 2000 +0200 +++ b/src/HOL/Tools/inductive_package.ML Thu Jul 13 23:13:10 2000 +0200 @@ -653,7 +653,7 @@ |> (if length cs < 2 then I else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)]) |> Theory.add_path rec_name - |> PureThy.add_defss_i [(("defs", def_terms), [])]; + |> PureThy.add_defss_i false [(("defs", def_terms), [])]; val mono = prove_mono setT fp_fun monos thy'