# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1254211082 -7200
# Node ID 18d8bcd769b3748b03e22195f56db4ff2105e0b9
# Parent  50f72361d0958fc94344657130c89f9b8d8fe2a2
Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.

diff -r 50f72361d095 -r 18d8bcd769b3 QuotMain.thy
--- 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