diff -r 329bc52b4b86 -r 750c5a47400b src/Sequents/simpdata.ML
--- a/src/Sequents/simpdata.ML	Thu Nov 24 20:45:34 2011 +0100
+++ b/src/Sequents/simpdata.ML	Thu Nov 24 21:01:06 2011 +0100
@@ -68,11 +68,11 @@
 (*No simprules, but basic infrastructure for simplification*)
 val LK_basic_ss =
   Simplifier.global_context @{theory} empty_ss
-    setsubgoaler asm_simp_tac
-    setSSolver (mk_solver "safe" safe_solver)
-    setSolver (mk_solver "unsafe" unsafe_solver)
-    setmksimps (K (map mk_meta_eq o atomize o gen_all))
-    setmkcong mk_meta_cong;
+  setSSolver (mk_solver "safe" safe_solver)
+  setSolver (mk_solver "unsafe" unsafe_solver)
+  |> Simplifier.set_subgoaler asm_simp_tac
+  |> Simplifier.set_mksimps (K (map mk_meta_eq o atomize o gen_all))
+  |> Simplifier.set_mkcong mk_meta_cong;
 
 val LK_simps =
    [triv_forall_equality, (* prunes params *)