src/HOL/Tools/inductive_package.ML
changeset 17261 193b84a70ca4
parent 17057 0934ac31985f
child 17325 d9d50222808e
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Sep 05 17:38:17 2005 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Sep 05 17:38:18 2005 +0200
     1.3 @@ -112,7 +112,7 @@
     1.4  
     1.5  (* get and put data *)
     1.6  
     1.7 -fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name);
     1.8 +val get_inductive = Symtab.curried_lookup o #1 o InductiveData.get;
     1.9  
    1.10  fun the_inductive thy name =
    1.11    (case get_inductive thy name of
    1.12 @@ -123,7 +123,7 @@
    1.13  
    1.14  fun put_inductives names info thy =
    1.15    let
    1.16 -    fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
    1.17 +    fun upd ((tab, monos), name) = (Symtab.curried_update_new (name, info) tab, monos);
    1.18      val tab_monos = Library.foldl upd (InductiveData.get thy, names)
    1.19        handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
    1.20    in InductiveData.put tab_monos thy end;