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