--- a/ProgTutorial/Package/Ind_Code.thy	Tue May 21 16:22:30 2019 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Wed May 22 12:38:51 2019 +0200
@@ -580,10 +580,14 @@
 \<close>
 ML %grayML\<open>fun chop_print params1 params2 prems1 prems2 ctxt =
 let 
- val pps = [Pretty.big_list "Params1 from the rule:" (map (pretty_cterm ctxt) params1), 
-            Pretty.big_list "Params2 from the predicate:" (map (pretty_cterm ctxt) params2), 
-            Pretty.big_list "Prems1 from the rule:" (map (pretty_thm ctxt) prems1),
-            Pretty.big_list "Prems2 from the predicate:" (map (pretty_thm ctxt) prems2)] 
+ val pps = [Pretty.big_list "Params1 from the rule:" 
+              (map (pretty_cterm ctxt) params1), 
+            Pretty.big_list "Params2 from the predicate:" 
+              (map (pretty_cterm ctxt) params2), 
+            Pretty.big_list "Prems1 from the rule:" 
+              (map (pretty_thm ctxt) prems1),
+            Pretty.big_list "Prems2 from the predicate:" 
+              (map (pretty_thm ctxt) prems2)] 
 in 
   pps |> Pretty.chunks
       |> Pretty.string_of
@@ -650,12 +654,11 @@
   \<open>fresh\<close>\\
   \<open>Prems1 from the rule:\<close>\\
   @{term "a \<noteq> b"}\\
-  @{text [break]
-"\<forall>fresh.
-      (\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)) \<longrightarrow>
-      (\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)) \<longrightarrow>
-      (\<forall>a t. fresh a (Lam a t)) \<longrightarrow> 
-      (\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> fresh a t"}\\
+  @{text "\<forall>fresh."}\\
+  @{text "(\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)) \<longrightarrow>"}\\
+  @{text "(\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)) \<longrightarrow>"}\\
+  @{text "(\<forall>a t. fresh a (Lam a t)) \<longrightarrow> "}\\
+  @{text "(\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> fresh a t"}\\
    \<open>Prems2 from the predicate:\<close>\\
    @{term "\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)"}\\
    @{term "\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)"}\\
@@ -682,7 +685,8 @@
     val (params1, params2) = chop (length cparams - length preds) cparams
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
-    resolve_tac  context [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1
+    resolve_tac context 
+      [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1
   end)\<close>
 
 text \<open>
@@ -755,7 +759,8 @@
     val (params1, params2) = chop (length cparams - length preds) cparams
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
-    resolve_tac context [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1
+    resolve_tac context 
+      [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1
     THEN EVERY1 (map (prepare_prem context params2 prems2) prems1)
   end)\<close>
 
@@ -854,7 +859,8 @@
     val (params1, params2) = chop (length cparams - length preds) cparams
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
-    resolve_tac context [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1
+    resolve_tac context 
+      [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1
     THEN EVERY1 (map (prepare_prem params2 prems2 context) prems1)
   end)\<close>