
diff -r 92173262cfe9 -r e6d920bea7a6 src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Thu May 12 18:17:32 2011 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Thu May 12 18:18:06 2011 +0200
@@ -330,15 +330,15 @@
 
 (*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
 ML {*
-fun record_auto_tac (cs, ss) =
-  auto_tac (cs addIs [ext] addSWrapper Record.split_wrapper,
-    ss addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
+fun record_auto_tac ctxt =
+  auto_tac (claset_of ctxt addIs [ext] addSWrapper Record.split_wrapper,
+    simpset_of ctxt addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
       @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
       @{thm o_apply}, @{thm Let_def}])
 *}
 
 method_setup record_auto = {*
-  Scan.succeed (fn ctxt => SIMPLE_METHOD (record_auto_tac (clasimpset_of ctxt)))
+  Scan.succeed (SIMPLE_METHOD o record_auto_tac)
 *} ""
 
 lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"




