--- a/QuotMain.thy	Tue Sep 29 09:26:22 2009 +0200
+++ b/QuotMain.thy	Tue Sep 29 09:58:02 2009 +0200
@@ -933,7 +933,7 @@
 ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *}
 ML {*
   Toplevel.program (fn () =>
-    Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2}
+    Drule.instantiate' [SOME cT, SOME cT, SOME @{ctyp bool}] [NONE, NONE, NONE, NONE, SOME (@{cpat "op ="})] @{thm arg_cong2}
   )
 *}
 
@@ -1132,7 +1132,7 @@
 thm list.induct
 
 ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm list.induct}))
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list.induct}))
 *}
 ML {*
   val goal =
@@ -1144,7 +1144,7 @@
   val cgoal = cterm_of @{theory} goal
   val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal)
 *}
-ML fset_defs_sym
+
 prove {* (Thm.term_of cgoal2) *}
   apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )
   apply (tactic {* foo_tac' @{context} 1 *})
@@ -1231,7 +1231,7 @@
 thm card1_suc
 
 ML {*
-  val m1_novars = snd(no_vars ((Context.Theory @{theory}),@{thm card1_suc}))
+  val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm card1_suc}))
 *}
 ML {*
   val goal = build_goal @{context} m1_novars consts @{typ "'a list"} mk_rep_abs