--- a/ProgTutorial/Package/Ind_Code.thy	Thu Oct 22 14:08:23 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Sun Oct 25 15:26:03 2009 +0100
@@ -135,8 +135,8 @@
 
 local_setup %gray {* fn lthy =>
 let
-  val def = defn_aux lthy fresh_orules 
-                             [fresh_pred] (fresh_pred, fresh_arg_tys)
+  val arg = (fresh_pred, fresh_arg_tys)
+  val def = defn_aux lthy fresh_orules [fresh_pred] arg
 in
   tracing (string_of_term lthy def); lthy
 end *}
@@ -239,9 +239,12 @@
   quantifiers. 
 *}
 
-ML{*fun inst_spec ctrm = 
-  Drule.instantiate' [SOME (ctyp_of_term ctrm)] [NONE, SOME ctrm] 
-    @{thm spec}*}
+ML{*fun inst_spec ctrm =
+let
+  val cty = ctyp_of_term ctrm
+in 
+  Drule.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec} 
+end*}
 
 text {*
   This helper function uses the function @{ML_ind instantiate' in Drule}
@@ -613,10 +616,10 @@
 *}
 ML{*fun chop_print params1 params2 prems1 prems2 ctxt =
 let 
-  val s = ["Params1 from the rule:", string_of_cterms ctxt params1] 
-        @ ["Params2 from the predicate:", string_of_cterms ctxt params2] 
-        @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1) 
-        @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2) 
+ val s = ["Params1 from the rule:", string_of_cterms ctxt params1] 
+       @ ["Params2 from the predicate:", string_of_cterms ctxt params2] 
+       @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1) 
+       @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2) 
 in 
   s |> cat_lines
     |> tracing