
diff -r aec7073d4645 -r daf404920ab9 ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Essential.thy	Tue May 14 11:10:53 2019 +0200
@@ -253,12 +253,13 @@
 
 text {*
   We can install this pretty printer with the function 
-  @{ML_ind addPrettyPrinter in PolyML} as follows.
+  @{ML_ind ML_system_pp} as follows.
 *}
 
-ML %grayML{*PolyML.addPrettyPrinter 
-  (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ)*}
-
+ML %grayML{*ML_system_pp
+  (fn _ => fn _ => Pretty.to_polyml o raw_pp_typ)*}
+
+ML \<open>@{typ "bool"}\<close>
 text {*
   Now the type bool is printed out in full detail.
 
@@ -286,8 +287,8 @@
   with the code
 *}
 
-ML %grayML{*PolyML.addPrettyPrinter 
-  (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy)*}
+ML %grayML{*ML_system_pp
+  (fn depth => fn _ => ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Theory.get_pure)*}
 
 text {*
   After that the types for booleans, lists and so on are printed out again 
@@ -817,7 +818,7 @@
 fun pretty_tyenv ctxt tyenv =
 let
   fun get_typs (v, (s, T)) = (TVar (v, s), T)
-  val print = pairself (pretty_typ ctxt)
+  val print = apply2 (pretty_typ ctxt)
 in 
   pretty_helper (print o get_typs) tyenv
 end*}
@@ -997,7 +998,7 @@
 ML %grayML{*fun pretty_env ctxt env =
 let
   fun get_trms (v, (T, t)) = (Var (v, T), t) 
-  val print = pairself (pretty_term ctxt)
+  val print = apply2 (pretty_term ctxt)
 in
   pretty_helper (print o get_trms) env 
 end*}
@@ -1080,8 +1081,8 @@
   val trm_list = 
         [@{term_pat \"?X\"}, @{term_pat \"a\"},
          @{term_pat \"f (\<lambda>a b. ?X a b) c\"},
-         @{term_pat \"\<lambda>a b. (op +) a b\"},
-         @{term_pat \"\<lambda>a. (op +) a ?Y\"}, @{term_pat \"?X ?Y\"},
+         @{term_pat \"\<lambda>a b. (+) a b\"},
+         @{term_pat \"\<lambda>a. (+) a ?Y\"}, @{term_pat \"?X ?Y\"},
          @{term_pat \"\<lambda>a b. ?X a b ?Y\"}, @{term_pat \"\<lambda>a. ?X a a\"},
          @{term_pat \"?X a\"}] 
 in
@@ -1106,7 +1107,7 @@
   val trm1 = @{term_pat \"\<lambda>x y. g (?X y x) (f (?Y x))\"}
   val trm2 = @{term_pat \"\<lambda>u v. g u (f u)\"}
   val init = Envir.empty 0
-  val env = Pattern.unify @{theory} (trm1, trm2) init
+  val env = Pattern.unify (Context.Proof @{context}) (trm1, trm2) init (* FIXME: Reference to generic context *)
 in
   pretty_env @{context} (Envir.term_env env)
 end"
@@ -1134,7 +1135,7 @@
   val trm2 = @{term "f a"}
   val init = Envir.empty 0
 in
-  Unify.unifiers (@{theory}, init, [(trm1, trm2)])
+  Unify.unifiers (Context.Proof @{context}, init, [(trm1, trm2)])
 end *}
 
 text {*
@@ -1171,7 +1172,7 @@
   val trm2 = @{term \"b\"}
   val init = Envir.empty 0
 in
-  Unify.unifiers (@{theory}, init, [(trm1, trm2)])
+  Unify.unifiers (Context.Proof @{context}, init, [(trm1, trm2)])
   |> Seq.pull
 end"
 "NONE"}
@@ -1215,12 +1216,12 @@
   @{text "?x"}.  Instantiation function for theorems is 
   @{ML_ind instantiate_normalize in Drule} from the structure 
   @{ML_struct Drule}. One problem, however, is
-  that this function expects the instantiations as lists of @{ML_type ctyp}
-  and @{ML_type cterm} pairs:
+  that this function expects the instantiations as lists of @{ML_type "((indexname * sort) * ctyp)"}
+  respective @{ML_type "(indexname * typ) * cterm"}:
 
   \begin{isabelle}
   @{ML instantiate_normalize in Drule}@{text ":"}
-  @{ML_type "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"}
+  @{ML_type "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> thm -> thm"}
   \end{isabelle}
 
   This means we have to transform the environment the higher-order matching 
@@ -1231,30 +1232,31 @@
   @{ML_type ctyp}-pairs with the function
 *}
 
-ML %grayML{*fun prep_trm thy (x, (T, t)) = 
-  (cterm_of thy (Var (x, T)), cterm_of thy t)*} 
+ML %grayML{*fun prep_trm ctxt (x, (T, t)) = 
+  ((x, T), Thm.cterm_of ctxt t)*} 
 
 text {*
   and into proper @{ML_type cterm}-pairs with
 *}
 
-ML %grayML{*fun prep_ty thy (x, (S, ty)) = 
-  (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)*}
+ML %grayML{*fun prep_ty ctxt (x, (S, ty)) = 
+  ((x, S), Thm.ctyp_of ctxt ty)*}
 
 text {*
   We can now calculate the instantiations from the matching function. 
 *}
 
-ML %linenosgray{*fun matcher_inst thy pat trm i = 
+ML %linenosgray{*fun matcher_inst ctxt pat trm i = 
 let
-  val univ = Unify.matchers thy [(pat, trm)] 
+  val univ = Unify.matchers (Context.Proof ctxt) [(pat, trm)] 
   val env = nth (Seq.list_of univ) i
   val tenv = Vartab.dest (Envir.term_env env)
   val tyenv = Vartab.dest (Envir.type_env env)
 in
-  (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
+  (map (prep_ty ctxt) tyenv, map (prep_trm ctxt) tenv)
 end*}
 
+ML \<open>Context.get_generic_context\<close>
 text {*
   In Line 3 we obtain the higher-order matcher. We assume there is a finite
   number of them and select the one we are interested in via the parameter 
@@ -1268,9 +1270,9 @@
 
   @{ML_response_fake [gray,display,linenos] 
   "let  
-  val pat = Logic.strip_imp_concl (prop_of @{thm spec})
+  val pat = Logic.strip_imp_concl (Thm.prop_of @{thm spec})
   val trm = @{term \"Trueprop (Q True)\"}
-  val inst = matcher_inst @{theory} pat trm 1
+  val inst = matcher_inst @{context} pat trm 1
 in
   Drule.instantiate_normalize inst @{thm spec}
 end"
@@ -1429,11 +1431,11 @@
   abstract objects that are guaranteed to be type-correct, and they can only
   be constructed via ``official interfaces''.
 
-  Certification is always relative to a theory context. For example you can 
+  Certification is always relative to a context. For example you can 
   write:
 
   @{ML_response_fake [display,gray] 
-  "cterm_of @{theory} @{term \"(a::nat) + b = c\"}" 
+  "Thm.cterm_of @{context} @{term \"(a::nat) + b = c\"}" 
   "a + b = c"}
 
   This can also be written with an antiquotation:
@@ -1457,7 +1459,7 @@
   val zero = @{term \"0::nat\"}
   val plus = Const (@{const_name plus}, [natT, natT] ---> natT)
 in
-  cterm_of @{theory} (plus $ zero $ zero)
+  Thm.cterm_of @{context} (plus $ zero $ zero)
 end" 
   "0 + 0"}
 
@@ -1466,7 +1468,7 @@
   the ML-level as follows:
 
   @{ML_response_fake [display,gray]
-  "ctyp_of @{theory} (@{typ nat} --> @{typ bool})"
+  "Thm.ctyp_of @{context} (@{typ nat} --> @{typ bool})"
   "nat \<Rightarrow> bool"}
 
   or with the antiquotation:
@@ -1575,8 +1577,18 @@
   Section~\ref{sec:local}).
 *}
 
+(*FIXME: add forward reference to Proof_Context.export *)
+ML %linenosgray{*val my_thm_vars =
+let
+  val ctxt0 = @{context}
+  val (_, ctxt1) = Variable.add_fixes ["P", "Q", "t"] ctxt0
+in
+  singleton (Proof_Context.export ctxt1 ctxt0) my_thm
+end*}
+
 local_setup %gray {*
-  Local_Theory.note ((@{binding "my_thm"}, []), [my_thm]) #> snd *}
+  Local_Theory.note ((@{binding "my_thm"}, []), [my_thm_vars]) #> snd *}
+
 
 text {*
   The third argument of @{ML note in Local_Theory} is the list of theorems we
@@ -1590,7 +1602,7 @@
 
 local_setup %gray {*
   Local_Theory.note ((@{binding "my_thm_simp"}, 
-       [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *}
+       [Attrib.internal (K Simplifier.simp_add)]), [my_thm_vars]) #> snd *}
 
 text {*
   Note that we have to use another name under which the theorem is stored,
@@ -1720,7 +1732,7 @@
   val eq = @{thm True_def}
 in
   (Thm.lhs_of eq, Thm.rhs_of eq) 
-  |> pairself (Pretty.string_of o (pretty_cterm @{context}))
+  |> apply2 (Pretty.string_of o (pretty_cterm @{context}))
 end"
   "(True, (\<lambda>x. x) = (\<lambda>x. x))"}
 
@@ -1795,7 +1807,7 @@
   @{ML_response_fake [display,gray]
   "let
   val thm = @{thm foo_test1}
-  val meta_eq = Object_Logic.atomize @{context} (cprop_of thm)
+  val meta_eq = Object_Logic.atomize @{context} (Thm.cprop_of thm)
 in
   Raw_Simplifier.rewrite_rule @{context} [meta_eq] thm
 end"
@@ -1819,7 +1831,7 @@
 ML %grayML{*fun atomize_thm ctxt thm =
 let
   val thm' = forall_intr_vars thm
-  val thm'' = Object_Logic.atomize ctxt (cprop_of thm')
+  val thm'' = Object_Logic.atomize ctxt (Thm.cprop_of thm')
 in
   Raw_Simplifier.rewrite_rule ctxt [thm''] thm'
 end*}
@@ -1839,7 +1851,7 @@
   @{ML_response_fake [display,gray]
   "let
   val trm = @{term \"P \<Longrightarrow> P::bool\"}
-  val tac = K (atac 1)
+  val tac = K (assume_tac @{context} 1)
 in
   Goal.prove @{context} [\"P\"] [] trm tac
 end"
@@ -1853,15 +1865,15 @@
   theorem by assumption. 
 
   There is also the possibility of proving multiple goals at the same time
-  using the function @{ML_ind prove_multi in Goal}. For this let us define the
+  using the function @{ML_ind prove_common in Goal}. For this let us define the
   following three helper functions.
 *}
 
 ML %grayML{*fun rep_goals i = replicate i @{prop "f x = f x"}
-fun rep_tacs i = replicate i (rtac @{thm refl})
+fun rep_tacs i = replicate i (resolve_tac @{context} [@{thm refl}])
 
 fun multi_test ctxt i =
-  Goal.prove_multi ctxt ["f", "x"] [] (rep_goals i) 
+  Goal.prove_common ctxt NONE ["f", "x"] [] (rep_goals i) 
     (K ((Goal.conjunction_tac THEN' RANGE (rep_tacs i)) 1))*}
 
 text {*
@@ -1872,7 +1884,7 @@
   "multi_test @{context} 3"
   "[\"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\"]"}
 
-  However you should be careful with @{ML prove_multi in Goal} and very
+  However you should be careful with @{ML prove_common in Goal} and very
   large goals. If you increase the counter in the code above to @{text 3000}, 
   you will notice that takes approximately ten(!) times longer than
   using @{ML map} and @{ML prove in Goal}.
@@ -1880,7 +1892,7 @@
   
 ML %grayML{*let 
   fun test_prove ctxt thm =
-    Goal.prove ctxt ["P", "x"] [] thm (K (rtac @{thm refl} 1))
+    Goal.prove ctxt ["P", "x"] [] thm (K (resolve_tac  @{context} [@{thm refl}] 1))
 in
   map (test_prove @{context}) (rep_goals 3000)
 end*}
@@ -1991,8 +2003,8 @@
 *}
 
 ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms 
-val get_names = map #1 o pthms_of 
-val get_pbodies = map (Future.join o #3) o pthms_of *}
+val get_names = (map Proofterm.thm_node_name) o pthms_of 
+val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of *}
 
 text {* 
   To see what their purpose is, consider the following three short proofs.
@@ -2248,7 +2260,7 @@
   this attribute is
 *}
 
-ML %grayML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}
+ML %grayML{*val my_symmetric = Thm.rule_attribute [] (fn _ => fn thm => thm RS @{thm sym})*}
 
 text {* 
   where the function @{ML_ind  rule_attribute in Thm} expects a function taking a 
@@ -2313,7 +2325,7 @@
 let
   fun RS_rev thm1 thm2 = thm2 RS thm1
 in
-  Thm.rule_attribute (fn _ => fn thm => fold RS_rev thms thm)
+  Thm.rule_attribute [] (fn _ => fn thm => fold RS_rev thms thm)
 end*}
 
 text {* 
@@ -2715,8 +2727,8 @@
   and type. For example:
 
   @{ML_response_fake [display,gray]
-  "tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}"
-  "The term \"op = (op = (op = (op = (op = op =))))\" has type 
+  "tell_type @{context} @{term \"(=) ((=) ((=) ((=) ((=) (=)))))\"}"
+  "The term \"(=) ((=) ((=) ((=) ((=) (=)))))\" has type 
 \"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
 
   \begin{readmore}




