--- a/ProgTutorial/Base.thy	Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Base.thy	Tue May 21 16:22:30 2019 +0200
@@ -3,6 +3,7 @@
         "~~/src/HOL/Library/LaTeXsugar"
 begin
 
+
 notation (latex output)
   Cons ("_ # _" [66,65] 65)
 

--- a/ProgTutorial/Essential.thy	Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Essential.thy	Tue May 21 16:22:30 2019 +0200
@@ -2098,10 +2098,10 @@
   Note also that applications of \<open>assumption\<close> do not
   count as a separate theorem, as you can see in the following code.
 
-  @{ML_matchresult [display,gray]
+  @{ML_response [display,gray]
   \<open>@{thm my_conjIb}
   |> get_all_names |> sort string_ord\<close>
-  \<open>["", "Pure.protectD", "Pure.protectI"]\<close>}
+  \<open>[ "Pure.protectD", "Pure.protectI"]\<close>}
 
 
   Interestingly, but not surprisingly, the proof of @{thm [source]

--- a/ProgTutorial/Package/Ind_Prelims.thy	Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Package/Ind_Prelims.thy	Tue May 21 16:22:30 2019 +0200
@@ -117,8 +117,8 @@
   by starting a subproof.
 \<close>
 
+  subgoal premises for P
 proof -
-  case (goal1 P)
   have p1: "R x y" by fact
   have p2: "\<forall>P. (\<forall>x. P x x) 
                   \<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P y z" by fact
@@ -155,6 +155,7 @@
     apply(rule p2[THEN spec[where x=P], THEN mp, THEN mp, OF r1, OF r2])
     done
 qed
+done
 
 text \<open>
   Now we are done. It might be surprising that we are not using the automatic
@@ -231,8 +232,8 @@
 shows "odd m \<Longrightarrow> even (Suc m)"
 apply (unfold odd_def even_def)
 apply (rule allI impI)+
+subgoal premises for P Q
 proof -
-  case (goal1 P Q)
   have p1: "\<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m)) 
                              \<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q m" by fact
   have r1: "P 0" by fact
@@ -244,6 +245,7 @@
 	           THEN mp, THEN mp, THEN mp, OF r1, OF r2, OF r3])
     done
 qed
+done
 
 text \<open>
   The interesting lines are 7 to 15. Again, the assumptions fall into two categories:
@@ -280,21 +282,23 @@
 shows "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
 apply (unfold accpart_def)
 apply (rule allI impI)+
+subgoal premises for P
 proof -
-  case (goal1 P)
   have p1: "\<And>y. R y x \<Longrightarrow> 
                    (\<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P y)" by fact
   have r1: "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x" by fact
   show "P x"
     apply(rule r1[rule_format])
+    subgoal premises for y
     proof -
-      case (goal1 y)
       have r1_prem: "R y x" by fact
       show "P y"
-	apply(rule p1[OF r1_prem, THEN spec[where x=P], THEN mp, OF r1])
+	    apply(rule p1[OF r1_prem, THEN spec[where x=P], THEN mp, OF r1])
       done
-  qed
+    qed
+    done
 qed
+done
 
 text \<open>
   As you can see, there are now two subproofs. The assumptions fall as usual into

--- a/ProgTutorial/Parsing.thy	Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Parsing.thy	Tue May 21 16:22:30 2019 +0200
@@ -1124,7 +1124,7 @@
 
    fun setup_proof (thm_name, src) lthy =
      let
-       val text = Input.source_content src
+       val (text, _) = Input.source_content src
        val trm = Code_Runtime.value lthy result_cookie ("", text)
      in
        Proof.theorem NONE (after_qed thm_name) [[(trm, [])]] lthy

--- a/ProgTutorial/Readme.thy	Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Readme.thy	Tue May 21 16:22:30 2019 +0200
@@ -160,7 +160,7 @@
 
 So as a rule of thumb, to facilitate result checking use prefer this order:
 \begin{enumerate}
- \item \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close>
+ \item \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close>    
  \item \<open>@{ML_response \<open>expr\<close> \<open>string\<close>}\<close>
  \item \<open>@{ML_matchresult_fake \<open>expr\<close> \<open>pat\<close>}\<close> or \<open>@{ML_response \<open>expr\<close>}\<close>
  \item \<open>@{ML_matchresult_fake_both \<open>expr\<close> \<open>pat\<close>}\<close>

--- a/ProgTutorial/Recipes/Antiquotes.thy	Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Recipes/Antiquotes.thy	Tue May 21 16:22:30 2019 +0200
@@ -40,7 +40,7 @@
 \<close>
 ML \<open>Input.pos_of\<close>
 ML%linenosgray\<open>fun ml_enclose bg en source =
-  ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;\<close>
+  ML_Lex.read bg @ ML_Lex.read_source source @ ML_Lex.read en;\<close>
 
 ML%linenosgray\<open>fun ml_val code_txt = (ml_enclose "val _ = " "" code_txt)
 
@@ -48,7 +48,7 @@
 let
   val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_val code_txt)
 in 
-   Pretty.str (Input.source_content code_txt)
+   Pretty.str (fst (Input.source_content code_txt))
 end
 
 val ml_checked_setup = Thy_Output.antiquotation_pretty_source @{binding "ML_checked"} (Scan.lift Args.text_input) output_ml\<close>
@@ -129,7 +129,7 @@
 \<close>
 
 ML%linenosgray\<open>fun ml_pat pat code =
-  ML_Lex.read "val" @ ML_Lex.read_source false pat @ ML_Lex.read " = " @ ML_Lex.read_source false code\<close>
+  ML_Lex.read "val" @ ML_Lex.read_source pat @ ML_Lex.read " = " @ ML_Lex.read_source code\<close>
 
 (*
 ML %grayML{*fun ml_pat code_txt pat =
@@ -154,8 +154,8 @@
 fun output_ml_resp ctxt (code_txt, pat) =
 let
   val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_pat pat code_txt)
-  val code = space_explode "\n" (Input.source_content code_txt)
-  val resp = add_resp (space_explode "\n" (Input.source_content pat))
+  val code = space_explode "\n" (fst (Input.source_content code_txt))
+  val resp = add_resp (space_explode "\n" (fst (Input.source_content pat)))
 in 
    Pretty.str (cat_lines (code @ resp))
 end

--- a/ProgTutorial/Tactical.thy	Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Tactical.thy	Tue May 21 16:22:30 2019 +0200
@@ -1029,7 +1029,8 @@
 
 ML %grayML\<open>fun select_tac' ctxt = 
   FIRST' [resolve_tac ctxt [@{thm conjI}], resolve_tac ctxt [@{thm impI}], 
-          resolve_tac ctxt [@{thm notI}], resolve_tac ctxt [@{thm allI}], K all_tac]\<close>text_raw\<open>\label{tac:selectprime}\<close>
+          resolve_tac ctxt [@{thm notI}], resolve_tac ctxt [@{thm allI}],
+          K all_tac]\<close>text_raw\<open>\label{tac:selectprime}\<close>
 
 text \<open>
   Since we like to mimic the behaviour of @{ML select_tac} as closely as possible, 
@@ -1473,6 +1474,7 @@
 
 ML %grayML\<open>val ss1 = put_simpset empty_ss @{context} addsimps [@{thm Diff_Int} RS @{thm eq_reflection}]\<close>
 
+thm "INF_cong"
 text \<open>
   Printing then out the components of the simpset gives:
 
@@ -1485,10 +1487,10 @@
 
   \footnote{\bf FIXME: Why does it print out ??.unknown}
 
-  Adding also the congruence rule @{thm [source] strong_INF_cong} 
+  Adding also the congruence rule @{thm [source] INF_cong} 
 \<close>
 
-ML %grayML\<open>val ss2 = ss1 |> Simplifier.add_cong (@{thm strong_INF_cong} RS @{thm eq_reflection})\<close>
+ML %grayML\<open>val ss2 = ss1 |> Simplifier.add_cong (@{thm INF_cong} RS @{thm eq_reflection})\<close>
 
 text \<open>
   gives
@@ -1499,7 +1501,7 @@
   ??.unknown: A1 - B1 \<inter> C1 \<equiv> A1 - B1 \<union> (A1 - C1)
 Congruences rules:
   Complete_Lattices.Inf_class.Inf: 
-    \<lbrakk>A1 = B1; \<And>x. x \<in> B1 =simp=> C1 x = D1 x\<rbrakk> \<Longrightarrow> INFIMUM A1 C1 \<equiv> INFIMUM B1 D1
+    \<lbrakk>A1 = B1; \<And>x. x \<in> B1 \<Longrightarrow> C1 x = D1 x\<rbrakk> \<Longrightarrow> Inf (C1 ` A1) \<equiv> Inf (D1 ` B1)
 Simproc patterns:\<close>}
 
   Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} 

--- a/ProgTutorial/antiquote_setup.ML	Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Tue May 21 16:22:30 2019 +0200
@@ -40,27 +40,27 @@
     ML_Lex.read "fn " @ ML_Lex.read (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) @
     ML_Lex.read " => (" @ src @ ML_Lex.read ")"
 
-fun ml_with_struct (NONE) src = ML_Lex.read_source false src 
+fun ml_with_struct (NONE) src = ML_Lex.read_source src 
   | ml_with_struct (SOME st) src = 
-      ML_Lex.read ("let open " ^ st ^ " in ") @ ML_Lex.read_source false src @ ML_Lex.read " end"
+      ML_Lex.read ("let open " ^ st ^ " in ") @ ML_Lex.read_source src @ ML_Lex.read " end"
 
 fun ml_val vs stru txt = 
     txt |> ml_with_struct stru
         |> ml_with_vars vs 
 
 fun ml_pat pat lhs =
-  ML_Lex.read "val " @ ML_Lex.read_source false pat @ 
+  ML_Lex.read "val " @ ML_Lex.read_source pat @ 
   ML_Lex.read " = " @
-  ML_Lex.read_source false lhs 
+  ML_Lex.read_source lhs 
 
 
 fun ml_struct src = 
   ML_Lex.read "functor DUMMY_FUNCTOR() = struct structure DUMMY = " @
-  ML_Lex.read_source false src @
+  ML_Lex.read_source src @
   ML_Lex.read " end"
 
 fun ml_type src = 
-  ML_Lex.read "val _ = NONE : (" @ ML_Lex.read_source false src @ ML_Lex.read ") option"
+  ML_Lex.read "val _ = NONE : (" @ ML_Lex.read_source src @ ML_Lex.read ") option"
 
 (* eval function *)
 fun eval_fn ctxt prep exp =
@@ -71,7 +71,7 @@
 let 
   fun compute exp = 
      let 
-       val input = ML_Lex.read "(let val r = " @ ML_Lex.read_source false exp @ 
+       val input = ML_Lex.read "(let val r = " @ ML_Lex.read_source exp @ 
                    ML_Lex.read " in (raise ERROR (@{make_string} r); ()) end )"
        val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of exp) input 
      in ""
@@ -85,7 +85,7 @@
 
 fun output_ml ctxt (src, (vs, stru)) =
   (eval_fn ctxt (ml_val vs stru) src; 
-   output ctxt (split_lines (Input.source_content src)))
+   output ctxt (split_lines (fst (Input.source_content src))))
  
 val parser_ml = Scan.lift (Args.text_input --
   (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] --
@@ -97,18 +97,18 @@
   val _ = writeln res
   val cnt = YXML.content_of res
   val pat = case opat of NONE => cnt 
-            | SOME p => p |>  Input.source_content 
+            | SOME p => p |>  fst o Input.source_content 
   val _ = if ignore_pat orelse Print_Mode.print_mode_active Latex.latexN orelse match_string is_sep pat cnt then () 
           else error (cat_lines ["Substring:", pat, "not contained in:", cnt])
   val out = if ignore_pat then cnt else pat
 in 
-  OutputTutorial.output ctxt ([Input.source_content src] @ [Library.prefix_lines "> " out])
+  OutputTutorial.output ctxt ([fst (Input.source_content src)] @ [Library.prefix_lines "> " out])
 end
 
 (* checks and prints a single ML-item and produces an index entry *)
 fun output_ml_ind ctxt (src, stru) =
 let 
-  val txt = Input.source_content src
+  val (txt,_) = Input.source_content src
 in
   (eval_fn ctxt (ml_val [] stru) src; 
    case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of
@@ -123,7 +123,7 @@
 (* checks and prints structures *)
 fun gen_output_struct outfn ctxt src = 
 let 
-  val txt = Input.source_content src
+  val (txt, _) = Input.source_content src
 in
   (eval_fn ctxt ml_struct src; 
    outfn {main = Code txt, minor = Plain "structure"} (split_lines txt))
@@ -135,7 +135,7 @@
 (* prints functors; no checks *)
 fun gen_output_funct outfn src = 
 let
-  val txt = Input.source_content src
+  val (txt, _) = Input.source_content src
 in
   (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt))
 end
@@ -146,7 +146,7 @@
 (* checks and prints types *)
 fun gen_output_type outfn ctxt src = 
 let 
-  val txt = Input.source_content src
+  val (txt, _) = Input.source_content src
 in
   (eval_fn ctxt ml_type src; 
    outfn {main = Code txt, minor = Plain "type"} (split_lines txt))
@@ -160,19 +160,19 @@
 (* checks and expression against a result pattern *)
 fun output_response ctxt (lhs, pat) = 
     (eval_fn ctxt (ml_pat pat) lhs;
-     output ctxt ((prefix_lines "" (Input.source_content lhs)) @ 
-       (prefix_lines "> " (dots_pat (Input.source_content pat)))))
+     output ctxt ((prefix_lines "" (fst (Input.source_content lhs))) @ 
+       (prefix_lines "> " (dots_pat (fst (Input.source_content pat))))))
 
 (* checks the expressions, but does not check it against a result pattern *)
 fun output_response_fake ctxt (lhs, pat) = 
     (eval_fn ctxt (ml_val [] NONE) lhs;
-     output ctxt ( (split_lines (Input.source_content lhs)) @ 
-        (prefix_lines "> " (dots_pat (Input.source_content pat)))))
+     output ctxt ( (split_lines (fst (Input.source_content lhs))) @ 
+        (prefix_lines "> " (dots_pat (fst (Input.source_content pat))))))
 
 (* checks the expressions, but does not check it against a result pattern *)
 fun ouput_response_fake_both ctxt (lhs, pat) = 
-    (output ctxt ((split_lines (Input.source_content lhs)) @ 
-     (prefix_lines "> " (dots_pat (Input.source_content pat)))))
+    (output ctxt ((split_lines (fst (Input.source_content lhs))) @ 
+     (prefix_lines "> " (dots_pat (fst ((Input.source_content pat)))))))
 
 val single_arg = Scan.lift (Args.text_input)
 val two_args   = Scan.lift (Args.text_input -- Args.text_input)
@@ -202,7 +202,7 @@
 
 fun check_file_exists _ src =
 let
-  val txt = Input.source_content src
+  val (txt, _) = Input.source_content src
 in
   (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) 
    then Latex.string (href_link txt)