--- a/ProgTutorial/Package/simple_inductive_package.ML	Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Package/simple_inductive_package.ML	Tue May 14 11:10:53 2019 +0200
@@ -49,8 +49,7 @@
 (* @chunk definitions *) 
 fun definitions rules params preds prednames syns arg_typess lthy =
 let
-  val thy = Proof_Context.theory_of lthy
-  val orules = map (Object_Logic.atomize_term thy) rules
+  val orules = map (Object_Logic.atomize_term lthy) rules
   val defs = 
     map (defs_aux lthy orules preds params) (preds ~~ arg_typess) 
 in
@@ -59,15 +58,18 @@
 (* @end *)
 
 fun inst_spec ct = 
-  Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec};
+  Thm.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec};
+
+fun dtac ctxt thm = dresolve_tac ctxt [thm]
+fun rtac ctxt thm = resolve_tac ctxt [thm]
 
 (* @chunk induction_tac *)
 fun induction_tac ctxt defs prems insts =
   EVERY1 [Object_Logic.full_atomize_tac ctxt,
           cut_facts_tac prems,
           rewrite_goal_tac ctxt defs,
-          EVERY' (map (dtac o inst_spec) insts),
-          assume_tac]
+          EVERY' (map (dtac ctxt o inst_spec) insts),
+          assume_tac ctxt]
 (* @end *)
 
 (* @chunk induction_rules *)
@@ -77,12 +79,10 @@
   
   val Ps = replicate (length preds) "P"
   val (newprednames, lthy3) = Variable.variant_fixes Ps lthy2
-
-  val thy = Proof_Context.theory_of lthy3			      
-
+ 
   val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss
   val newpreds = map Free (newprednames ~~ Tss')
-  val cnewpreds = map (cterm_of thy) newpreds
+  val cnewpreds = map (Thm.cterm_of lthy3) newpreds
   val rules' = map (subst_free (preds ~~ newpreds)) rules
 
   fun prove_induction ((pred, newpred), Ts)  =
@@ -110,17 +110,17 @@
 
 (* @chunk subproof1 *) 
 fun subproof2 prem params2 prems2 =  
- SUBPROOF (fn {prems, ...} =>
+ SUBPROOF (fn {prems, context, ...} =>
   let
     val prem' = prems MRS prem;
     val prem'' = 
-       case prop_of prem' of
+       case Thm.prop_of prem' of
            _ $ (Const (@{const_name All}, _) $ _) =>
              prem' |> all_elims params2 
                    |> imp_elims prems2
          | _ => prem';
   in 
-    rtac prem'' 1 
+    rtac context prem'' 1 
   end)
 (* @end *)
 
@@ -131,7 +131,7 @@
     val (prems1, prems2) = chop (length prems - length rules) prems;
     val (params1, params2) = chop (length params - length preds) (map snd params);
   in
-    rtac (Object_Logic.rulify ctxt' (all_elims params1 (nth prems2 i))) 1 
+    rtac ctxt' (Object_Logic.rulify ctxt' (all_elims params1 (nth prems2 i))) 1 
     THEN
     EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)
   end)
@@ -140,7 +140,7 @@
 fun introductions_tac defs rules preds i ctxt =
   EVERY1 [Object_Logic.rulify_tac ctxt,
           rewrite_goal_tac ctxt defs,
-          REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
+          REPEAT o (resolve_tac ctxt [@{thm allI},@{thm impI}]),
           subproof1 rules preds i ctxt]
 
 
@@ -194,16 +194,15 @@
     |> snd
 end
 (* @end *)
-
+val _ = Proof_Context.read_stmt
 (* @chunk read_specification *)
 fun read_specification' vars specs lthy =
 let 
-  val specs' = map (fn (a, s) => (a, [s])) specs
-  val ((varst, specst), _) = 
-                   Specification.read_specification vars specs' lthy
-  val specst' = map (apsnd the_single) specst
+  val specs' = map (fn (a, s) => ((a, s), [],[])) specs
+  val ((varst, specst),_) = 
+                   Specification.read_multi_specs vars specs' lthy
 in   
-  (varst, specst')
+  (varst, specst)
 end 
 (* @end *)
 
@@ -221,7 +220,7 @@
 (* @chunk parser *)
 val spec_parser = 
    Parse.opt_target --
-   Parse.fixes -- 
+   Parse.vars -- 
    Parse.for_fixes --
    Scan.optional 
      (Parse.$$$ "where" |--
@@ -234,10 +233,11 @@
 val specification =
   spec_parser >>
     (fn (((loc, preds), params), specs) =>
-      Toplevel.local_theory loc (add_inductive preds params specs))
+      Toplevel.local_theory NONE loc (add_inductive preds params specs))
 
-val _ = Outer_Syntax.command @{command_spec "simple_inductive"} "define inductive predicates"
+val _ = Outer_Syntax.command @{command_keyword "simple_inductive"} "define inductive predicates"
           specification
+
 (* @end *)
 
 end;