# HG changeset patch # User haftmann # Date 1258366483 -3600 # Node ID 93a4a42603a7cecd2de05f4182ca4a5bb0345a94 # Parent 68841fb382e0c2ff0d4c69d5c19b6f740d02ad58# Parent b45d3b8cc74eae3dadcb6184beefa16055dca979 merged diff -r 68841fb382e0 -r 93a4a42603a7 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Mon Nov 16 11:03:14 2009 +0100 +++ b/src/Pure/Isar/code.ML Mon Nov 16 11:14:43 2009 +0100 @@ -268,7 +268,7 @@ of SOME cs => invoke_purge_all thy (complete_class_params thy cs) (! data) | NONE => empty_data))) thy; -val purge_data = (Code_Data.map o apsnd) (K (Unsynchronized.ref empty_data)); +val purge_data = (Code_Data.map o apsnd) (fn _ => Unsynchronized.ref empty_data); fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, [])), [])))