src/ZF/Tools/induct_tacs.ML
changeset 17223 430edc6b7826
parent 17057 0934ac31985f
child 17314 04e21a27c0ad
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Thu Sep 01 18:48:54 2005 +0200
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Thu Sep 01 22:15:10 2005 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4  struct
     1.5  
     1.6  fun datatype_info thy name =
     1.7 -  (case Symtab.lookup (DatatypesData.get thy, name) of
     1.8 +  (case Symtab.curried_lookup (DatatypesData.get thy) name of
     1.9      SOME info => info
    1.10    | NONE => error ("Unknown datatype " ^ quote name));
    1.11  
    1.12 @@ -163,14 +163,12 @@
    1.13      val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
    1.14  
    1.15    in
    1.16 -      thy |> Theory.add_path (Sign.base_name big_rec_name)
    1.17 -          |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
    1.18 -          |> DatatypesData.put
    1.19 -              (Symtab.update
    1.20 -               ((big_rec_name, dt_info), DatatypesData.get thy))
    1.21 -          |> ConstructorsData.put
    1.22 -               (foldr Symtab.update (ConstructorsData.get thy) con_pairs)
    1.23 -          |> Theory.parent_path
    1.24 +    thy
    1.25 +    |> Theory.add_path (Sign.base_name big_rec_name)
    1.26 +    |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
    1.27 +    |> DatatypesData.put (Symtab.curried_update (big_rec_name, dt_info) (DatatypesData.get thy))
    1.28 +    |> ConstructorsData.put (fold_rev Symtab.curried_update con_pairs (ConstructorsData.get thy))
    1.29 +    |> Theory.parent_path
    1.30    end;
    1.31  
    1.32  fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =