src/HOL/Tools/recfun_codegen.ML
changeset 17261 193b84a70ca4
parent 17203 29b2563f5c11
child 17412 e26cb20ef0cc
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Mon Sep 05 17:38:17 2005 +0200
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Mon Sep 05 17:38:18 2005 +0200
     1.3 @@ -42,8 +42,7 @@
     1.4      val (s, _) = const_of (prop_of thm);
     1.5    in
     1.6      if Pattern.pattern (lhs_of thm) then
     1.7 -      (CodegenData.put (Symtab.update ((s,
     1.8 -        (thm, optmod) :: getOpt (Symtab.lookup (tab, s), [])), tab)) thy, thm)
     1.9 +      (CodegenData.put (Symtab.curried_update_multi (s, (thm, optmod)) tab) thy, thm)
    1.10      else (warn thm; p)
    1.11    end handle TERM _ => (warn thm; p);
    1.12  
    1.13 @@ -51,10 +50,10 @@
    1.14    let
    1.15      val tab = CodegenData.get thy;
    1.16      val (s, _) = const_of (prop_of thm);
    1.17 -  in case Symtab.lookup (tab, s) of
    1.18 +  in case Symtab.curried_lookup tab s of
    1.19        NONE => p
    1.20 -    | SOME thms => (CodegenData.put (Symtab.update ((s,
    1.21 -        gen_rem (eq_thm o apfst fst) (thms, thm)), tab)) thy, thm)
    1.22 +    | SOME thms => (CodegenData.put (Symtab.curried_update (s,
    1.23 +        gen_rem (eq_thm o apfst fst) (thms, thm)) tab) thy, thm)
    1.24    end handle TERM _ => (warn thm; p);
    1.25  
    1.26  fun del_redundant thy eqs [] = eqs
    1.27 @@ -65,7 +64,7 @@
    1.28      in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end;
    1.29  
    1.30  fun get_equations thy defs (s, T) =
    1.31 -  (case Symtab.lookup (CodegenData.get thy, s) of
    1.32 +  (case Symtab.curried_lookup (CodegenData.get thy) s of
    1.33       NONE => ([], "")
    1.34     | SOME thms => 
    1.35         let val thms' = del_redundant thy []