# HG changeset patch
# User wenzelm
# Date 1395355114 -3600
# Node ID 713ae0c9e652c042d3b6eac5b5f8d07e213bff8c
# Parent  67a5f004583da890fb2136e64981e9b2cb5573b2# Parent  083b41092afe2b0c5de96fbd6058c9b210b4af2d
merged

diff -r 67a5f004583d -r 713ae0c9e652 NEWS
--- a/NEWS	Thu Mar 20 15:13:55 2014 -0700
+++ b/NEWS	Thu Mar 20 23:38:34 2014 +0100
@@ -25,6 +25,15 @@
 supports input methods via ` (backquote), or << and >> (double angle
 brackets).
 
+* More static checking of proof methods, which allows the system to
+form a closure over the concrete syntax.  Method arguments should be
+processed in the original proof context as far as possible, before
+operating on the goal state.  In any case, the standard discipline for
+subgoal-addressing needs to be observed: no subgoals or a subgoal
+number that is out of range produces an empty result sequence, not an
+exception.  Potential INCOMPATIBILITY for non-conformant tactical
+proof tools.
+
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
diff -r 67a5f004583d -r 713ae0c9e652 src/HOL/Library/Lattice_Algebras.thy
--- a/src/HOL/Library/Lattice_Algebras.thy	Thu Mar 20 15:13:55 2014 -0700
+++ b/src/HOL/Library/Lattice_Algebras.thy	Thu Mar 20 23:38:34 2014 +0100
@@ -18,9 +18,10 @@
 
 lemma add_inf_distrib_right: "inf a b + c = inf (a + c) (b + c)"
 proof -
-  have "c + inf a b = inf (c+a) (c+b)"
+  have "c + inf a b = inf (c + a) (c + b)"
     by (simp add: add_inf_distrib_left)
-  thus ?thesis by (simp add: add_commute)
+  then show ?thesis
+    by (simp add: add_commute)
 qed
 
 end
@@ -37,10 +38,12 @@
   apply (rule add_le_imp_le_left [of "a"], simp only: add_assoc[symmetric], simp)+
   done
 
-lemma add_sup_distrib_right: "sup a b + c = sup (a+c) (b+c)"
+lemma add_sup_distrib_right: "sup a b + c = sup (a + c) (b + c)"
 proof -
-  have "c + sup a b = sup (c+a) (c+b)" by (simp add: add_sup_distrib_left)
-  thus ?thesis by (simp add: add_commute)
+  have "c + sup a b = sup (c+a) (c+b)"
+    by (simp add: add_sup_distrib_left)
+  then show ?thesis
+    by (simp add: add_commute)
 qed
 
 end
@@ -54,10 +57,10 @@
 lemmas add_sup_inf_distribs =
   add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
 
-lemma inf_eq_neg_sup: "inf a b = - sup (-a) (-b)"
+lemma inf_eq_neg_sup: "inf a b = - sup (- a) (- b)"
 proof (rule inf_unique)
   fix a b c :: 'a
-  show "- sup (-a) (-b) \<le> a"
+  show "- sup (- a) (- b) \<le> a"
     by (rule add_le_imp_le_right [of _ "sup (uminus a) (uminus b)"])
       (simp, simp add: add_sup_distrib_left)
   show "- sup (-a) (-b) \<le> b"
@@ -68,26 +71,27 @@
     by (subst neg_le_iff_le [symmetric]) (simp add: le_supI)
 qed
 
-lemma sup_eq_neg_inf: "sup a b = - inf (-a) (-b)"
+lemma sup_eq_neg_inf: "sup a b = - inf (- a) (- b)"
 proof (rule sup_unique)
   fix a b c :: 'a
-  show "a \<le> - inf (-a) (-b)"
+  show "a \<le> - inf (- a) (- b)"
     by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"])
       (simp, simp add: add_inf_distrib_left)
-  show "b \<le> - inf (-a) (-b)"
+  show "b \<le> - inf (- a) (- b)"
     by (rule add_le_imp_le_right [of _ "inf (uminus a) (uminus b)"])
       (simp, simp add: add_inf_distrib_left)
   assume "a \<le> c" "b \<le> c"
-  then show "- inf (-a) (-b) \<le> c" by (subst neg_le_iff_le [symmetric]) (simp add: le_infI)
+  then show "- inf (- a) (- b) \<le> c"
+    by (subst neg_le_iff_le [symmetric]) (simp add: le_infI)
 qed
 
-lemma neg_inf_eq_sup: "- inf a b = sup (-a) (-b)"
+lemma neg_inf_eq_sup: "- inf a b = sup (- a) (- b)"
   by (simp add: inf_eq_neg_sup)
 
 lemma diff_inf_eq_sup: "a - inf b c = a + sup (- b) (- c)"
   using neg_inf_eq_sup [of b c, symmetric] by simp
 
-lemma neg_sup_eq_inf: "- sup a b = inf (-a) (-b)"
+lemma neg_sup_eq_inf: "- sup a b = inf (- a) (- b)"
   by (simp add: sup_eq_neg_inf)
 
 lemma diff_sup_eq_inf: "a - sup b c = a + inf (- b) (- c)"
@@ -95,13 +99,14 @@
 
 lemma add_eq_inf_sup: "a + b = sup a b + inf a b"
 proof -
-  have "0 = - inf 0 (a-b) + inf (a-b) 0"
+  have "0 = - inf 0 (a - b) + inf (a - b) 0"
     by (simp add: inf_commute)
-  hence "0 = sup 0 (b-a) + inf (a-b) 0"
+  then have "0 = sup 0 (b - a) + inf (a - b) 0"
     by (simp add: inf_eq_neg_sup)
-  hence "0 = (-a + sup a b) + (inf a b + (-b))"
+  then have "0 = (- a + sup a b) + (inf a b + (- b))"
     by (simp only: add_sup_distrib_left add_inf_distrib_right) simp
-  then show ?thesis by (simp add: algebra_simps)
+  then show ?thesis
+    by (simp add: algebra_simps)
 qed
 
 
@@ -115,10 +120,13 @@
 
 lemma pprt_neg: "pprt (- x) = - nprt x"
 proof -
-  have "sup (- x) 0 = sup (- x) (- 0)" unfolding minus_zero ..
-  also have "\<dots> = - inf x 0" unfolding neg_inf_eq_sup ..
+  have "sup (- x) 0 = sup (- x) (- 0)"
+    unfolding minus_zero ..
+  also have "\<dots> = - inf x 0"
+    unfolding neg_inf_eq_sup ..
   finally have "sup (- x) 0 = - inf x 0" .
-  then show ?thesis unfolding pprt_def nprt_def .
+  then show ?thesis
+    unfolding pprt_def nprt_def .
 qed
 
 lemma nprt_neg: "nprt (- x) = - pprt x"
@@ -172,20 +180,26 @@
 lemma sup_0_imp_0: "sup a (- a) = 0 \<Longrightarrow> a = 0"
 proof -
   {
-    fix a::'a
-    assume hyp: "sup a (-a) = 0"
-    hence "sup a (-a) + a = a" by (simp)
-    hence "sup (a+a) 0 = a" by (simp add: add_sup_distrib_right)
-    hence "sup (a+a) 0 <= a" by (simp)
-    hence "0 <= a" by (blast intro: order_trans inf_sup_ord)
+    fix a :: 'a
+    assume hyp: "sup a (- a) = 0"
+    then have "sup a (- a) + a = a"
+      by simp
+    then have "sup (a + a) 0 = a"
+      by (simp add: add_sup_distrib_right)
+    then have "sup (a + a) 0 \<le> a"
+      by simp
+    then have "0 \<le> a"
+      by (blast intro: order_trans inf_sup_ord)
   }
   note p = this
   assume hyp:"sup a (-a) = 0"
-  hence hyp2:"sup (-a) (-(-a)) = 0" by (simp add: sup_commute)
-  from p[OF hyp] p[OF hyp2] show "a = 0" by simp
+  then have hyp2:"sup (-a) (-(-a)) = 0"
+    by (simp add: sup_commute)
+  from p[OF hyp] p[OF hyp2] show "a = 0"
+    by simp
 qed
 
-lemma inf_0_imp_0: "inf a (-a) = 0 \<Longrightarrow> a = 0"
+lemma inf_0_imp_0: "inf a (- a) = 0 \<Longrightarrow> a = 0"
   apply (simp add: inf_eq_neg_sup)
   apply (simp add: sup_commute)
   apply (erule sup_0_imp_0)
@@ -206,24 +220,32 @@
 lemma zero_le_double_add_iff_zero_le_single_add [simp]:
   "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
 proof
-  assume "0 <= a + a"
-  hence a:"inf (a+a) 0 = 0" by (simp add: inf_commute inf_absorb1)
-  have "(inf a 0)+(inf a 0) = inf (inf (a+a) 0) a" (is "?l=_")
+  assume "0 \<le> a + a"
+  then have a: "inf (a + a) 0 = 0"
+    by (simp add: inf_commute inf_absorb1)
+  have "inf a 0 + inf a 0 = inf (inf (a + a) 0) a"  (is "?l=_")
     by (simp add: add_sup_inf_distribs inf_aci)
-  hence "?l = 0 + inf a 0" by (simp add: a, simp add: inf_commute)
-  hence "inf a 0 = 0" by (simp only: add_right_cancel)
-  then show "0 <= a" unfolding le_iff_inf by (simp add: inf_commute)
+  then have "?l = 0 + inf a 0"
+    by (simp add: a, simp add: inf_commute)
+  then have "inf a 0 = 0"
+    by (simp only: add_right_cancel)
+  then show "0 \<le> a"
+    unfolding le_iff_inf by (simp add: inf_commute)
 next
-  assume a: "0 <= a"
-  show "0 <= a + a" by (simp add: add_mono[OF a a, simplified])
+  assume a: "0 \<le> a"
+  show "0 \<le> a + a"
+    by (simp add: add_mono[OF a a, simplified])
 qed
 
 lemma double_zero [simp]: "a + a = 0 \<longleftrightarrow> a = 0"
 proof
   assume assm: "a + a = 0"
-  then have "a + a + - a = - a" by simp
-  then have "a + (a + - a) = - a" by (simp only: add_assoc)
-  then have a: "- a = a" by simp
+  then have "a + a + - a = - a"
+    by simp
+  then have "a + (a + - a) = - a"
+    by (simp only: add_assoc)
+  then have a: "- a = a"
+    by simp
   show "a = 0"
     apply (rule antisym)
     apply (unfold neg_le_iff_le [symmetric, of a])
@@ -236,7 +258,8 @@
     done
 next
   assume "a = 0"
-  then show "a + a = 0" by simp
+  then show "a + a = 0"
+    by simp
 qed
 
 lemma zero_less_double_add_iff_zero_less_single_add [simp]: "0 < a + a \<longleftrightarrow> 0 < a"
@@ -261,19 +284,23 @@
 lemma double_add_le_zero_iff_single_add_le_zero [simp]:
   "a + a \<le> 0 \<longleftrightarrow> a \<le> 0"
 proof -
-  have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)" by (subst le_minus_iff, simp)
+  have "a + a \<le> 0 \<longleftrightarrow> 0 \<le> - (a + a)"
+    by (subst le_minus_iff, simp)
   moreover have "\<dots> \<longleftrightarrow> a \<le> 0"
     by (simp only: minus_add_distrib zero_le_double_add_iff_zero_le_single_add) simp
-  ultimately show ?thesis by blast
+  ultimately show ?thesis
+    by blast
 qed
 
 lemma double_add_less_zero_iff_single_less_zero [simp]:
   "a + a < 0 \<longleftrightarrow> a < 0"
 proof -
-  have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)" by (subst less_minus_iff, simp)
+  have "a + a < 0 \<longleftrightarrow> 0 < - (a + a)"
+    by (subst less_minus_iff) simp
   moreover have "\<dots> \<longleftrightarrow> a < 0"
     by (simp only: minus_add_distrib zero_less_double_add_iff_zero_less_single_add) simp
-  ultimately show ?thesis by blast
+  ultimately show ?thesis
+    by blast
 qed
 
 declare neg_inf_eq_sup [simp] neg_sup_eq_inf [simp] diff_inf_eq_sup [simp] diff_sup_eq_inf [simp]
@@ -281,17 +308,19 @@
 lemma le_minus_self_iff: "a \<le> - a \<longleftrightarrow> a \<le> 0"
 proof -
   from add_le_cancel_left [of "uminus a" "plus a a" zero]
-  have "(a <= -a) = (a+a <= 0)"
+  have "a \<le> - a \<longleftrightarrow> a + a \<le> 0"
     by (simp add: add_assoc[symmetric])
-  thus ?thesis by simp
+  then show ?thesis
+    by simp
 qed
 
 lemma minus_le_self_iff: "- a \<le> a \<longleftrightarrow> 0 \<le> a"
 proof -
   from add_le_cancel_left [of "uminus a" zero "plus a a"]
-  have "(-a <= a) = (0 <= a+a)"
+  have "- a \<le> a \<longleftrightarrow> 0 \<le> a + a"
     by (simp add: add_assoc[symmetric])
-  thus ?thesis by simp
+  then show ?thesis
+    by simp
 qed
 
 lemma zero_le_iff_zero_nprt: "0 \<le> a \<longleftrightarrow> nprt a = 0"
@@ -314,7 +343,8 @@
 
 end
 
-lemmas add_sup_inf_distribs = add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
+lemmas add_sup_inf_distribs =
+  add_inf_distrib_right add_inf_distrib_left add_sup_distrib_right add_sup_distrib_left
 
 
 class lattice_ab_group_add_abs = lattice_ab_group_add + abs +
@@ -325,11 +355,15 @@
 proof -
   have "0 \<le> \<bar>a\<bar>"
   proof -
-    have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>" by (auto simp add: abs_lattice)
-    show ?thesis by (rule add_mono [OF a b, simplified])
+    have a: "a \<le> \<bar>a\<bar>" and b: "- a \<le> \<bar>a\<bar>"
+      by (auto simp add: abs_lattice)
+    show ?thesis
+      by (rule add_mono [OF a b, simplified])
   qed
-  then have "0 \<le> sup a (- a)" unfolding abs_lattice .
-  then have "sup (sup a (- a)) 0 = sup a (- a)" by (rule sup_absorb1)
+  then have "0 \<le> sup a (- a)"
+    unfolding abs_lattice .
+  then have "sup (sup a (- a)) 0 = sup a (- a)"
+    by (rule sup_absorb1)
   then show ?thesis
     by (simp add: add_sup_inf_distribs ac_simps pprt_def nprt_def abs_lattice)
 qed
@@ -347,7 +381,8 @@
   have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
     by (simp add: abs_lattice le_supI)
   fix a b
-  show "0 \<le> \<bar>a\<bar>" by simp
+  show "0 \<le> \<bar>a\<bar>"
+    by simp
   show "a \<le> \<bar>a\<bar>"
     by (auto simp add: abs_lattice)
   show "\<bar>-a\<bar> = \<bar>a\<bar>"
@@ -359,14 +394,20 @@
   }
   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   proof -
-    have g:"abs a + abs b = sup (a+b) (sup (-a-b) (sup (-a+b) (a + (-b))))" (is "_=sup ?m ?n")
+    have g: "\<bar>a\<bar> + \<bar>b\<bar> = sup (a + b) (sup (- a - b) (sup (- a + b) (a + (- b))))"
+      (is "_=sup ?m ?n")
       by (simp add: abs_lattice add_sup_inf_distribs sup_aci ac_simps)
-    have a: "a + b <= sup ?m ?n" by simp
-    have b: "- a - b <= ?n" by simp
-    have c: "?n <= sup ?m ?n" by simp
-    from b c have d: "-a-b <= sup ?m ?n" by (rule order_trans)
-    have e:"-a-b = -(a+b)" by simp
-    from a d e have "abs(a+b) <= sup ?m ?n"
+    have a: "a + b \<le> sup ?m ?n"
+      by simp
+    have b: "- a - b \<le> ?n"
+      by simp
+    have c: "?n \<le> sup ?m ?n"
+      by simp
+    from b c have d: "- a - b \<le> sup ?m ?n"
+      by (rule order_trans)
+    have e: "- a - b = - (a + b)"
+      by simp
+    from a d e have "\<bar>a + b\<bar> \<le> sup ?m ?n"
       apply -
       apply (drule abs_leI)
       apply (simp_all only: algebra_simps ac_simps minus_add)
@@ -379,7 +420,7 @@
 end
 
 lemma sup_eq_if:
-  fixes a :: "'a\<Colon>{lattice_ab_group_add, linorder}"
+  fixes a :: "'a::{lattice_ab_group_add, linorder}"
   shows "sup a (- a) = (if a < 0 then - a else a)"
 proof -
   note add_le_cancel_right [of a a "- a", symmetric, simplified]
@@ -388,18 +429,23 @@
 qed
 
 lemma abs_if_lattice:
-  fixes a :: "'a\<Colon>{lattice_ab_group_add_abs, linorder}"
+  fixes a :: "'a::{lattice_ab_group_add_abs, linorder}"
   shows "\<bar>a\<bar> = (if a < 0 then - a else a)"
   by auto
 
 lemma estimate_by_abs:
-  "a + b <= (c::'a::lattice_ab_group_add_abs) \<Longrightarrow> a <= c + abs b"
+  fixes a b c :: "'a::lattice_ab_group_add_abs"
+  shows "a + b \<le> c \<Longrightarrow> a \<le> c + \<bar>b\<bar>"
 proof -
-  assume "a+b <= c"
-  then have "a <= c+(-b)" by (simp add: algebra_simps)
-  have "(-b) <= abs b" by (rule abs_ge_minus_self)
-  then have "c + (- b) \<le> c + \<bar>b\<bar>" by (rule add_left_mono)
-  with `a \<le> c + (- b)` show ?thesis by (rule order_trans)
+  assume "a + b \<le> c"
+  then have "a \<le> c + (- b)"
+    by (simp add: algebra_simps)
+  have "- b \<le> \<bar>b\<bar>"
+    by (rule abs_ge_minus_self)
+  then have "c + (- b) \<le> c + \<bar>b\<bar>"
+    by (rule add_left_mono)
+  with `a \<le> c + (- b)` show ?thesis
+    by (rule order_trans)
 qed
 
 class lattice_ring = ordered_ring + lattice_ab_group_add_abs
@@ -410,15 +456,17 @@
 
 end
 
-lemma abs_le_mult: "abs (a * b) \<le> (abs a) * (abs (b::'a::lattice_ring))"
+lemma abs_le_mult:
+  fixes a b :: "'a::lattice_ring"
+  shows "\<bar>a * b\<bar> \<le> \<bar>a\<bar> * \<bar>b\<bar>"
 proof -
   let ?x = "pprt a * pprt b - pprt a * nprt b - nprt a * pprt b + nprt a * nprt b"
   let ?y = "pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
-  have a: "(abs a) * (abs b) = ?x"
+  have a: "\<bar>a\<bar> * \<bar>b\<bar> = ?x"
     by (simp only: abs_prts[of a] abs_prts[of b] algebra_simps)
   {
     fix u v :: 'a
-    have bh: "\<lbrakk>u = a; v = b\<rbrakk> \<Longrightarrow>
+    have bh: "u = a \<Longrightarrow> v = b \<Longrightarrow>
               u * v = pprt a * pprt b + pprt a * nprt b +
                       nprt a * pprt b + nprt a * nprt b"
       apply (subst prts[of u], subst prts[of v])
@@ -426,16 +474,22 @@
       done
   }
   note b = this[OF refl[of a] refl[of b]]
-  have xy: "- ?x <= ?y"
+  have xy: "- ?x \<le> ?y"
     apply simp
-    apply (metis (full_types) add_increasing add_uminus_conv_diff lattice_ab_group_add_class.minus_le_self_iff minus_add_distrib mult_nonneg_nonneg mult_nonpos_nonpos nprt_le_zero zero_le_pprt)
+    apply (metis (full_types) add_increasing add_uminus_conv_diff
+      lattice_ab_group_add_class.minus_le_self_iff minus_add_distrib mult_nonneg_nonneg
+      mult_nonpos_nonpos nprt_le_zero zero_le_pprt)
     done
-  have yx: "?y <= ?x"
+  have yx: "?y \<le> ?x"
     apply simp
-    apply (metis (full_types) add_nonpos_nonpos add_uminus_conv_diff lattice_ab_group_add_class.le_minus_self_iff minus_add_distrib mult_nonneg_nonpos mult_nonpos_nonneg nprt_le_zero zero_le_pprt)
+    apply (metis (full_types) add_nonpos_nonpos add_uminus_conv_diff
+      lattice_ab_group_add_class.le_minus_self_iff minus_add_distrib mult_nonneg_nonpos
+      mult_nonpos_nonneg nprt_le_zero zero_le_pprt)
     done
-  have i1: "a*b <= abs a * abs b" by (simp only: a b yx)
-  have i2: "- (abs a * abs b) <= a*b" by (simp only: a b xy)
+  have i1: "a * b \<le> \<bar>a\<bar> * \<bar>b\<bar>"
+    by (simp only: a b yx)
+  have i2: "- (\<bar>a\<bar> * \<bar>b\<bar>) \<le> a * b"
+    by (simp only: a b xy)
   show ?thesis
     apply (rule abs_leI)
     apply (simp add: i1)
@@ -445,37 +499,38 @@
 
 instance lattice_ring \<subseteq> ordered_ring_abs
 proof
-  fix a b :: "'a\<Colon> lattice_ring"
+  fix a b :: "'a::lattice_ring"
   assume a: "(0 \<le> a \<or> a \<le> 0) \<and> (0 \<le> b \<or> b \<le> 0)"
-  show "abs (a*b) = abs a * abs b"
+  show "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
   proof -
-    have s: "(0 <= a*b) | (a*b <= 0)"
-      apply (auto)
+    have s: "(0 \<le> a * b) \<or> (a * b \<le> 0)"
+      apply auto
       apply (rule_tac split_mult_pos_le)
-      apply (rule_tac contrapos_np[of "a*b <= 0"])
-      apply (simp)
+      apply (rule_tac contrapos_np[of "a * b \<le> 0"])
+      apply simp
       apply (rule_tac split_mult_neg_le)
-      apply (insert a)
-      apply (blast)
+      using a
+      apply blast
       done
     have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
       by (simp add: prts[symmetric])
     show ?thesis
-    proof cases
-      assume "0 <= a * b"
+    proof (cases "0 \<le> a * b")
+      case True
       then show ?thesis
         apply (simp_all add: mulprts abs_prts)
-        apply (insert a)
+        using a
         apply (auto simp add:
           algebra_simps
           iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
           iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
-          apply(drule (1) mult_nonneg_nonpos[of a b], simp)
-          apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
+        apply(drule (1) mult_nonneg_nonpos[of a b], simp)
+        apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
         done
     next
-      assume "~(0 <= a*b)"
-      with s have "a*b <= 0" by simp
+      case False
+      with s have "a * b \<le> 0"
+        by simp
       then show ?thesis
         apply (simp_all add: mulprts abs_prts)
         apply (insert a)
@@ -488,11 +543,12 @@
 qed
 
 lemma mult_le_prts:
-  assumes "a1 <= (a::'a::lattice_ring)"
-    and "a <= a2"
-    and "b1 <= b"
-    and "b <= b2"
-  shows "a * b <=
+  fixes a b :: "'a::lattice_ring"
+  assumes "a1 \<le> a"
+    and "a \<le> a2"
+    and "b1 \<le> b"
+    and "b \<le> b2"
+  shows "a * b \<le>
     pprt a2 * pprt b2 + pprt a1 * nprt b2 + nprt a2 * pprt b1 + nprt a1 * nprt b1"
 proof -
   have "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
@@ -501,31 +557,31 @@
     done
   then have "a * b = pprt a * pprt b + pprt a * nprt b + nprt a * pprt b + nprt a * nprt b"
     by (simp add: algebra_simps)
-  moreover have "pprt a * pprt b <= pprt a2 * pprt b2"
+  moreover have "pprt a * pprt b \<le> pprt a2 * pprt b2"
     by (simp_all add: assms mult_mono)
-  moreover have "pprt a * nprt b <= pprt a1 * nprt b2"
+  moreover have "pprt a * nprt b \<le> pprt a1 * nprt b2"
   proof -
-    have "pprt a * nprt b <= pprt a * nprt b2"
+    have "pprt a * nprt b \<le> pprt a * nprt b2"
       by (simp add: mult_left_mono assms)
-    moreover have "pprt a * nprt b2 <= pprt a1 * nprt b2"
+    moreover have "pprt a * nprt b2 \<le> pprt a1 * nprt b2"
       by (simp add: mult_right_mono_neg assms)
     ultimately show ?thesis
       by simp
   qed
-  moreover have "nprt a * pprt b <= nprt a2 * pprt b1"
+  moreover have "nprt a * pprt b \<le> nprt a2 * pprt b1"
   proof -
-    have "nprt a * pprt b <= nprt a2 * pprt b"
+    have "nprt a * pprt b \<le> nprt a2 * pprt b"
       by (simp add: mult_right_mono assms)
-    moreover have "nprt a2 * pprt b <= nprt a2 * pprt b1"
+    moreover have "nprt a2 * pprt b \<le> nprt a2 * pprt b1"
       by (simp add: mult_left_mono_neg assms)
     ultimately show ?thesis
       by simp
   qed
-  moreover have "nprt a * nprt b <= nprt a1 * nprt b1"
+  moreover have "nprt a * nprt b \<le> nprt a1 * nprt b1"
   proof -
-    have "nprt a * nprt b <= nprt a * nprt b1"
+    have "nprt a * nprt b \<le> nprt a * nprt b1"
       by (simp add: mult_left_mono_neg assms)
-    moreover have "nprt a * nprt b1 <= nprt a1 * nprt b1"
+    moreover have "nprt a * nprt b1 \<le> nprt a1 * nprt b1"
       by (simp add: mult_right_mono_neg assms)
     ultimately show ?thesis
       by simp
@@ -537,36 +593,41 @@
 qed
 
 lemma mult_ge_prts:
-  assumes "a1 <= (a::'a::lattice_ring)"
-    and "a <= a2"
-    and "b1 <= b"
-    and "b <= b2"
-  shows "a * b >=
+  fixes a b :: "'a::lattice_ring"
+  assumes "a1 \<le> a"
+    and "a \<le> a2"
+    and "b1 \<le> b"
+    and "b \<le> b2"
+  shows "a * b \<ge>
     nprt a1 * pprt b2 + nprt a2 * nprt b2 + pprt a1 * pprt b1 + pprt a2 * nprt b1"
 proof -
-  from assms have a1:"- a2 <= -a"
+  from assms have a1: "- a2 \<le> -a"
     by auto
-  from assms have a2: "-a <= -a1"
+  from assms have a2: "- a \<le> -a1"
     by auto
-  from mult_le_prts[of "-a2" "-a" "-a1" "b1" b "b2", OF a1 a2 assms(3) assms(4), simplified nprt_neg pprt_neg]
-  have le: "- (a * b) <= - nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1"
+  from mult_le_prts[of "- a2" "- a" "- a1" "b1" b "b2",
+    OF a1 a2 assms(3) assms(4), simplified nprt_neg pprt_neg]
+  have le: "- (a * b) \<le> - nprt a1 * pprt b2 + - nprt a2 * nprt b2 +
+    - pprt a1 * pprt b1 + - pprt a2 * nprt b1"
     by simp
-  then have "-(- nprt a1 * pprt b2 + - nprt a2 * nprt b2 + - pprt a1 * pprt b1 + - pprt a2 * nprt b1) <= a * b"
+  then have "- (- nprt a1 * pprt b2 + - nprt a2 * nprt b2 +
+      - pprt a1 * pprt b1 + - pprt a2 * nprt b1) \<le> a * b"
     by (simp only: minus_le_iff)
-  then show ?thesis by (simp add: algebra_simps)
+  then show ?thesis
+    by (simp add: algebra_simps)
 qed
 
 instance int :: lattice_ring
 proof
   fix k :: int
-  show "abs k = sup k (- k)"
+  show "\<bar>k\<bar> = sup k (- k)"
     by (auto simp add: sup_int_def)
 qed
 
 instance real :: lattice_ring
 proof
   fix a :: real
-  show "abs a = sup a (- a)"
+  show "\<bar>a\<bar> = sup a (- a)"
     by (auto simp add: sup_real_def)
 qed
 
diff -r 67a5f004583d -r 713ae0c9e652 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Thu Mar 20 15:13:55 2014 -0700
+++ b/src/HOL/Nominal/Nominal.thy	Thu Mar 20 23:38:34 2014 +0100
@@ -3638,13 +3638,15 @@
 (* tactics for generating fresh names and simplifying fresh_funs *)
 ML_file "nominal_fresh_fun.ML"
 
-method_setup generate_fresh = 
-  {* setup_generate_fresh *} 
-  {* tactic to generate a name fresh for all the variables in the goal *}
-
-method_setup fresh_fun_simp = 
-  {* setup_fresh_fun_simp *} 
-  {* tactic to delete one inner occurence of fresh_fun *}
+method_setup generate_fresh = {*
+  Args.type_name {proper = true, strict = true} >>
+    (fn s => fn ctxt => SIMPLE_METHOD (generate_fresh_tac ctxt s))
+*} "generate a name fresh for all the variables in the goal"
+
+method_setup fresh_fun_simp = {*
+  Scan.lift (Args.parens (Args.$$$ "no_asm") >> K true || Scan.succeed false) >>
+    (fn b => fn ctxt => SIMPLE_METHOD' (fresh_fun_tac ctxt b))
+*} "delete one inner occurence of fresh_fun"
 
 
 (************************************************)
diff -r 67a5f004583d -r 713ae0c9e652 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 20 15:13:55 2014 -0700
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 20 23:38:34 2014 +0100
@@ -5,7 +5,7 @@
 a tactic to analyse instances of the fresh_fun.
 *)
 
-(* FIXME proper ML structure *)
+(* FIXME proper ML structure! *)
 
 (* FIXME res_inst_tac mostly obsolete, cf. Subgoal.FOCUS *)
 
@@ -52,12 +52,11 @@
 (* A tactic to generate a name fresh for  all the free *)
 (* variables and parameters of the goal                *)
 
-fun generate_fresh_tac atom_name i thm =
+fun generate_fresh_tac ctxt atom_name = SUBGOAL (fn (goal, _) =>
  let
-   val thy = theory_of_thm thm;
+   val thy = Proof_Context.theory_of ctxt;
 (* the parsing function returns a qualified name, we get back the base name *)
    val atom_basename = Long_Name.base_name atom_name;
-   val goal = nth (prems_of thm) (i - 1);
    val ps = Logic.strip_params goal;
    val Ts = rev (map snd ps);
    fun is_of_fs_name T = Sign.of_sort thy (T, [Sign.intern_class thy ("fs_"^atom_basename)]);
@@ -76,11 +75,12 @@
 (* find the variable we want to instantiate *)
    val x = hd (Misc_Legacy.term_vars (prop_of exists_fresh'));
  in
+   fn st =>
    (cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
    rtac fs_name_thm 1 THEN
-   etac exE 1) thm
-  handle List.Empty  => all_tac thm (* if we collected no variables then we do nothing *)
-  end;
+   etac exE 1) st
+  handle List.Empty  => all_tac st (* if we collected no variables then we do nothing *)
+ end) 1;
 
 fun get_inner_fresh_fun (Bound j) = NONE
   | get_inner_fresh_fun (v as Free _) = NONE
@@ -97,15 +97,14 @@
 (* This tactic generates a fresh name of the atom type *)
 (* given by the innermost fresh_fun                    *)
 
-fun generate_fresh_fun_tac i thm =
+fun generate_fresh_fun_tac ctxt = SUBGOAL (fn (goal, _) =>
   let
-    val goal = nth (prems_of thm) (i - 1);
     val atom_name_opt = get_inner_fresh_fun goal;
   in
   case atom_name_opt of
-    NONE => all_tac thm
-  | SOME atom_name  => generate_fresh_tac atom_name i thm
-  end
+    NONE => all_tac
+  | SOME atom_name  => generate_fresh_tac ctxt atom_name
+  end) 1;
 
 (* Two substitution tactics which looks for the innermost occurence in
    one assumption or in the conclusion *)
@@ -123,24 +122,23 @@
   curry (curry (FIRST' (map uncurry (map uncurry (map subst_inner_asm_tac_aux
             (1 upto Thm.nprems_of th)))))) ctxt th;
 
-fun fresh_fun_tac ctxt no_asm i thm =
+fun fresh_fun_tac ctxt no_asm = SUBGOAL (fn (goal, i) =>
   (* Find the variable we instantiate *)
   let
-    val thy = theory_of_thm thm;
+    val thy = Proof_Context.theory_of ctxt;
     val abs_fresh = Global_Theory.get_thms thy "abs_fresh";
     val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app";
     val simp_ctxt =
       ctxt addsimps (fresh_prod :: abs_fresh)
       addsimps fresh_perm_app;
     val x = hd (tl (Misc_Legacy.term_vars (prop_of exI)));
-    val goal = nth (prems_of thm) (i-1);
     val atom_name_opt = get_inner_fresh_fun goal;
     val n = length (Logic.strip_params goal);
     (* Here we rely on the fact that the variable introduced by generate_fresh_tac *)
     (* is the last one in the list, the inner one *)
   in
   case atom_name_opt of
-    NONE => all_tac thm
+    NONE => all_tac
   | SOME atom_name =>
   let
     val atom_basename = Long_Name.base_name atom_name;
@@ -173,21 +171,7 @@
     (subst_inner_asm_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i)))
     ORELSE
     (subst_inner_tac ctxt fresh_fun_app' i THEN (RANGE post_rewrite_tacs i))) st
-  end)) thm
-
+  end))
   end
-  end
+  end)
 
-(* syntax for options, given "(no_asm)" will give back true, without
-   gives back false *)
-val options_syntax =
-    (Args.parens (Args.$$$ "no_asm") >> (K true)) ||
-     (Scan.succeed false);
-
-fun setup_generate_fresh x =
-  (Args.goal_spec -- Args.type_name {proper = true, strict = true} >>
-    (fn (quant, s) => K (SIMPLE_METHOD'' quant (generate_fresh_tac s)))) x;
-
-fun setup_fresh_fun_simp x =
-  (Scan.lift options_syntax >> (fn b => fn ctxt => SIMPLE_METHOD' (fresh_fun_tac ctxt b))) x;
-
diff -r 67a5f004583d -r 713ae0c9e652 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Thu Mar 20 15:13:55 2014 -0700
+++ b/src/HOL/Nominal/nominal_permeq.ML	Thu Mar 20 23:38:34 2014 +0100
@@ -142,7 +142,7 @@
 (* stac contains the simplifiation tactic that is *)
 (* applied (see (no_asm) options below            *)
 fun perm_simp_gen stac dyn_thms eqvt_thms ctxt i = 
-    ("general simplification of permutations", fn st =>
+    ("general simplification of permutations", fn st => SUBGOAL (fn _ =>
     let
        val ctxt' = ctxt
          addsimps (maps (dynamic_thms st) dyn_thms @ eqvt_thms)
@@ -150,8 +150,8 @@
          |> fold Simplifier.del_cong weak_congs
          |> fold Simplifier.add_cong strong_congs
     in
-      stac ctxt' i st
-    end);
+      stac ctxt' i
+    end) i st);
 
 (* general simplification of permutations and permutation that arose from eqvt-problems *)
 fun perm_simp stac ctxt = 
diff -r 67a5f004583d -r 713ae0c9e652 src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Thu Mar 20 15:13:55 2014 -0700
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Thu Mar 20 23:38:34 2014 +0100
@@ -174,7 +174,7 @@
 
 (** The Main Function **)
 
-fun lex_order_tac quiet ctxt solve_tac (st: thm) =
+fun lex_order_tac quiet ctxt solve_tac st = SUBGOAL (fn _ =>
   let
     val thy = Proof_Context.theory_of ctxt
     val ((_ $ (_ $ rel)) :: tl) = prems_of st
@@ -187,26 +187,27 @@
     val table = (* 2: create table *)
       map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
   in
-    case search_table table of
-      NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
-    | SOME order =>
-      let
-        val clean_table = map (fn x => map (nth x) order) table
-        val relation = mk_measures domT (map (nth measure_funs) order)
-        val _ =
-          if not quiet then
-            Pretty.writeln (Pretty.block
-              [Pretty.str "Found termination order:", Pretty.brk 1,
-                Pretty.quote (Syntax.pretty_term ctxt relation)])
-          else ()
-
-      in (* 4: proof reconstruction *)
-        st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
-        THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
-        THEN (rtac @{thm "wf_empty"} 1)
-        THEN EVERY (map prove_row clean_table))
-      end
-  end
+    fn st =>
+      case search_table table of
+        NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
+      | SOME order =>
+        let
+          val clean_table = map (fn x => map (nth x) order) table
+          val relation = mk_measures domT (map (nth measure_funs) order)
+          val _ =
+            if not quiet then
+              Pretty.writeln (Pretty.block
+                [Pretty.str "Found termination order:", Pretty.brk 1,
+                  Pretty.quote (Syntax.pretty_term ctxt relation)])
+            else ()
+  
+        in (* 4: proof reconstruction *)
+          st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
+          THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
+          THEN (rtac @{thm "wf_empty"} 1)
+          THEN EVERY (map prove_row clean_table))
+        end
+  end) 1 st;
 
 fun lexicographic_order_tac quiet ctxt =
   TRY (Function_Common.apply_termination_rule ctxt 1) THEN
diff -r 67a5f004583d -r 713ae0c9e652 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Thu Mar 20 15:13:55 2014 -0700
+++ b/src/HOL/Tools/Function/termination.ML	Thu Mar 20 23:38:34 2014 +0100
@@ -272,10 +272,10 @@
 
 in
 
-fun wf_union_tac ctxt st =
+fun wf_union_tac ctxt st = SUBGOAL (fn _ =>
   let
     val thy = Proof_Context.theory_of ctxt
-    val cert = cterm_of (theory_of_thm st)
+    val cert = cterm_of thy
     val ((_ $ (_ $ rel)) :: ineqs) = prems_of st
 
     fun mk_compr ineq =
@@ -304,8 +304,8 @@
   in
     (PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
      THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i)
-     THEN rewrite_goal_tac ctxt Un_aci_simps 1) st  (* eliminate duplicates *)
-  end
+     THEN rewrite_goal_tac ctxt Un_aci_simps 1)  (* eliminate duplicates *)
+  end) 1 st
 
 end
 
diff -r 67a5f004583d -r 713ae0c9e652 src/HOL/Tools/coinduction.ML
--- a/src/HOL/Tools/coinduction.ML	Thu Mar 20 15:13:55 2014 -0700
+++ b/src/HOL/Tools/coinduction.ML	Thu Mar 20 23:38:34 2014 +0100
@@ -40,19 +40,20 @@
     (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o etac thin_rl)) i st
   end;
 
-fun coinduction_tac ctxt raw_vars opt_raw_thm prems st =
+fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _, _) =>
   let
     val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
     fun find_coinduct t = 
       Induct.find_coinductP ctxt t @
       (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default [])
-    val raw_thm = case opt_raw_thm
-      of SOME raw_thm => raw_thm
-       | NONE => st |> prems_of |> hd |> Logic.strip_assums_concl |> find_coinduct |> hd;
+    val raw_thm =
+      (case opt_raw_thm of
+        SOME raw_thm => raw_thm
+      | NONE => goal |> Logic.strip_assums_concl |> find_coinduct |> hd);
     val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1
     val cases = Rule_Cases.get raw_thm |> fst
   in
-    NO_CASES (HEADGOAL (
+    HEADGOAL (
       Object_Logic.rulify_tac ctxt THEN'
       Method.insert_tac prems THEN'
       Object_Logic.atomize_prems_tac ctxt THEN'
@@ -110,10 +111,10 @@
                         unfold_thms_tac ctxt eqs
                       end)) ctxt)))])
         end) ctxt) THEN'
-      K (prune_params_tac ctxt))) st
-    |> Seq.maps (fn (_, st) =>
+      K (prune_params_tac ctxt))
+    #> Seq.maps (fn st =>
       CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, prop_of st) cases) all_tac st)
-  end;
+  end));
 
 local
 
diff -r 67a5f004583d -r 713ae0c9e652 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Thu Mar 20 15:13:55 2014 -0700
+++ b/src/HOL/Topological_Spaces.thy	Thu Mar 20 23:38:34 2014 +0100
@@ -373,7 +373,7 @@
 qed
 
 ML {*
-  fun eventually_elim_tac ctxt thms thm =
+  fun eventually_elim_tac ctxt thms = SUBGOAL_CASES (fn (_, _, st) =>
     let
       val thy = Proof_Context.theory_of ctxt
       val mp_thms = thms RL [@{thm eventually_rev_mp}]
@@ -381,11 +381,11 @@
         (@{thm allI} RS @{thm always_eventually})
         |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
         |> fold (fn _ => fn thm => @{thm impI} RS thm) thms
-      val cases_prop = prop_of (raw_elim_thm RS thm)
+      val cases_prop = prop_of (raw_elim_thm RS st)
       val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])])
     in
-      CASES cases (rtac raw_elim_thm 1) thm
-    end
+      CASES cases (rtac raw_elim_thm 1)
+    end) 1
 *}
 
 method_setup eventually_elim = {*
diff -r 67a5f004583d -r 713ae0c9e652 src/HOL/ex/Antiquote.thy
--- a/src/HOL/ex/Antiquote.thy	Thu Mar 20 15:13:55 2014 -0700
+++ b/src/HOL/ex/Antiquote.thy	Thu Mar 20 23:38:34 2014 +0100
@@ -13,14 +13,14 @@
   syntax.
 *}
 
-definition var :: "'a => ('a => nat) => nat"  ("VAR _" [1000] 999)
+definition var :: "'a \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"  ("VAR _" [1000] 999)
   where "var x env = env x"
 
-definition Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
+definition Expr :: "(('a \<Rightarrow> nat) \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"
   where "Expr exp env = exp env"
 
 syntax
-  "_Expr" :: "'a => 'a"  ("EXPR _" [1000] 999)
+  "_Expr" :: "'a \<Rightarrow> 'a"  ("EXPR _" [1000] 999)
 
 parse_translation {*
   [Syntax_Trans.quote_antiquote_tr
diff -r 67a5f004583d -r 713ae0c9e652 src/HOL/ex/Multiquote.thy
--- a/src/HOL/ex/Multiquote.thy	Thu Mar 20 15:13:55 2014 -0700
+++ b/src/HOL/ex/Multiquote.thy	Thu Mar 20 23:38:34 2014 +0100
@@ -14,8 +14,8 @@
 *}
 
 syntax
-  "_quote" :: "'b => ('a => 'b)"    ("\<guillemotleft>_\<guillemotright>" [0] 1000)
-  "_antiquote" :: "('a => 'b) => 'b"    ("\<acute>_" [1000] 1000)
+  "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"    ("\<guillemotleft>_\<guillemotright>" [0] 1000)
+  "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"    ("\<acute>_" [1000] 1000)
 
 parse_translation {*
   let
@@ -43,8 +43,8 @@
 
 text {* advanced examples *}
 term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright>\<guillemotright>"
-term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright> o \<acute>f\<guillemotright>"
-term "\<guillemotleft>\<acute>(f o \<acute>g)\<guillemotright>"
-term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>(f o \<acute>g)\<guillemotright>\<guillemotright>"
+term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright> \<circ> \<acute>f\<guillemotright>"
+term "\<guillemotleft>\<acute>(f \<circ> \<acute>g)\<guillemotright>"
+term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>(f \<circ> \<acute>g)\<guillemotright>\<guillemotright>"
 
 end
diff -r 67a5f004583d -r 713ae0c9e652 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Mar 20 15:13:55 2014 -0700
+++ b/src/Pure/Isar/method.ML	Thu Mar 20 23:38:34 2014 +0100
@@ -64,7 +64,6 @@
   val finish_text: text option * bool -> text
   val print_methods: Proof.context -> unit
   val check_name: Proof.context -> xstring * Position.T -> string
-  val check_src: Proof.context -> src -> src
   val method: Proof.context -> src -> Proof.context -> method
   val method_cmd: Proof.context -> src -> Proof.context -> method
   val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
@@ -339,7 +338,7 @@
 (* check *)
 
 fun check_name ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_methods ctxt);
-fun check_src ctxt src = #1 (Args.check_src ctxt (get_methods ctxt) src);
+fun check_src ctxt src = Args.check_src ctxt (get_methods ctxt) src;
 
 
 (* get methods *)
@@ -348,7 +347,14 @@
   let val table = get_methods ctxt
   in fn src => #1 (Name_Space.get table (#1 (Args.name_of_src src))) src end;
 
-fun method_cmd ctxt = method ctxt o check_src ctxt;
+fun method_closure ctxt src0 =
+  let
+    val (src1, meth) = check_src ctxt src0;
+    val src2 = Args.init_assignable src1;
+    val _ = Seq.pull (apply (method ctxt src2) ctxt [] (Goal.protect 0 Drule.dummy_thm));
+  in Args.closure src2 end;
+
+fun method_cmd ctxt = method ctxt o method_closure ctxt;
 
 
 (* method setup *)
diff -r 67a5f004583d -r 713ae0c9e652 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Thu Mar 20 15:13:55 2014 -0700
+++ b/src/Pure/Isar/rule_cases.ML	Thu Mar 20 23:38:34 2014 +0100
@@ -12,7 +12,7 @@
   type cases_tactic
   val CASES: cases -> tactic -> cases_tactic
   val NO_CASES: tactic -> cases_tactic
-  val SUBGOAL_CASES: ((term * int) -> cases_tactic) -> int -> cases_tactic
+  val SUBGOAL_CASES: ((term * int * thm) -> cases_tactic) -> int -> cases_tactic
   val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
 end
 
@@ -190,7 +190,7 @@
 
 fun SUBGOAL_CASES tac i st =
   (case try Logic.nth_prem (i, Thm.prop_of st) of
-    SOME goal => tac (goal, i) st
+    SOME goal => tac (goal, i, st) st
   | NONE => Seq.empty);
 
 fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
diff -r 67a5f004583d -r 713ae0c9e652 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Mar 20 15:13:55 2014 -0700
+++ b/src/Pure/ML/ml_context.ML	Thu Mar 20 23:38:34 2014 +0100
@@ -191,3 +191,7 @@
 
 end;
 
+fun use s =
+  ML_Context.eval_file true (Path.explode s)
+    handle ERROR msg => (writeln msg; error "ML error");
+
diff -r 67a5f004583d -r 713ae0c9e652 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Mar 20 15:13:55 2014 -0700
+++ b/src/Pure/ROOT.ML	Thu Mar 20 23:38:34 2014 +0100
@@ -226,7 +226,6 @@
 (*ML with context and antiquotations*)
 use "ML/ml_context.ML";
 use "ML/ml_antiquotation.ML";
-val use = ML_Context.eval_file true o Path.explode;
 (*^^^^^ end of ML bootstrap 1 ^^^^^*)
 
 (*basic proof engine*)
diff -r 67a5f004583d -r 713ae0c9e652 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Thu Mar 20 15:13:55 2014 -0700
+++ b/src/Pure/pure_thy.ML	Thu Mar 20 23:38:34 2014 +0100
@@ -20,6 +20,8 @@
 val tycon = Lexicon.mark_type;
 val const = Lexicon.mark_const;
 
+val qualify = Binding.qualify true Context.PureN;
+
 
 (* application syntax variants *)
 
@@ -207,11 +209,11 @@
   #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
   #> Sign.parse_translation Syntax_Trans.pure_parse_translation
   #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
+  #> Sign.add_consts_i
+   [(qualify (Binding.name "term"), typ "'a => prop", NoSyn),
+    (qualify (Binding.name "sort_constraint"), typ "'a itself => prop", NoSyn),
+    (qualify (Binding.name "conjunction"), typ "prop => prop => prop", NoSyn)]
   #> Sign.local_path
-  #> Sign.add_consts_i
-   [(Binding.name "term", typ "'a => prop", NoSyn),
-    (Binding.name "sort_constraint", typ "'a itself => prop", NoSyn),
-    (Binding.name "conjunction", typ "prop => prop => prop", NoSyn)]
   #> (Global_Theory.add_defs false o map Thm.no_attributes)
    [(Binding.name "prop_def", prop "(CONST prop :: prop => prop) (A::prop) == A::prop"),
     (Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
@@ -219,9 +221,6 @@
       prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST TYPE :: 'a itself) ==\
       \ (CONST Pure.term :: 'a itself => prop) (CONST TYPE :: 'a itself)"),
     (Binding.name "conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
-  #> Sign.hide_const false "Pure.term"
-  #> Sign.hide_const false "Pure.sort_constraint"
-  #> Sign.hide_const false "Pure.conjunction"
   #> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd
   #> fold (fn (a, prop) =>
       snd o Thm.add_axiom_global (Binding.name a, prop)) Proofterm.equality_axms);
diff -r 67a5f004583d -r 713ae0c9e652 src/Pure/tactical.ML
--- a/src/Pure/tactical.ML	Thu Mar 20 15:13:55 2014 -0700
+++ b/src/Pure/tactical.ML	Thu Mar 20 23:38:34 2014 +0100
@@ -334,15 +334,14 @@
 (*Returns all states that have changed in subgoal i, counted from the LAST
   subgoal.  For stac, for example.*)
 fun CHANGED_GOAL tac i st =
-    let val np = Thm.nprems_of st
-        val d = np-i                 (*distance from END*)
-        val t = Thm.term_of (Thm.cprem_of st i)
-        fun diff st' =
-            Thm.nprems_of st' - d <= 0   (*the subgoal no longer exists*)
-            orelse
-             not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
-    in  Seq.filter diff (tac i st)  end
-    handle General.Subscript => Seq.empty  (*no subgoal i*);
+  SUBGOAL (fn (t, _) =>
+    let
+      val np = Thm.nprems_of st;
+      val d = np - i;  (*distance from END*)
+      fun diff st' =
+        Thm.nprems_of st' - d <= 0 orelse  (*the subgoal no longer exists*)
+        not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))));
+    in Seq.filter diff o tac i end) i st;
 
 (*Returns all states where some subgoals have been solved.  For
   subgoal-based tactics this means subgoal i has been solved
diff -r 67a5f004583d -r 713ae0c9e652 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Thu Mar 20 15:13:55 2014 -0700
+++ b/src/Tools/induct.ML	Thu Mar 20 23:38:34 2014 +0100
@@ -741,71 +741,71 @@
 type case_data = (((string * string list) * string list) list * int);
 
 fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
-  let
-    val thy = Proof_Context.theory_of ctxt;
-
-    val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
-    val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
-
-    fun inst_rule (concls, r) =
-      (if null insts then `Rule_Cases.get r
-       else (align_left "Rule has fewer conclusions than arguments given"
-          (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
-        |> maps (prep_inst ctxt align_right (atomize_term thy))
-        |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
-      |> mod_cases thy
-      |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
-
-    val ruleq =
-      (case opt_rule of
-        SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
-      | NONE =>
-          (get_inductP ctxt facts @
-            map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
-          |> map_filter (Rule_Cases.mutual_rule ctxt)
-          |> tap (trace_rules ctxt inductN o map #2)
-          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
-
-    fun rule_cases ctxt rule cases =
-      let
-        val rule' = Rule_Cases.internalize_params rule;
-        val rule'' = rule' |> simp ? simplified_rule ctxt;
-        val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
-        val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
-      in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') cases' end;
-  in
-    (fn i => fn st =>
-      ruleq
-      |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
-      |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
-        (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
-          (CONJUNCTS (ALLGOALS
-            let
-              val adefs = nth_list atomized_defs (j - 1);
-              val frees = fold (Term.add_frees o Thm.prop_of) adefs [];
-              val xs = nth_list arbitrary (j - 1);
-              val k = nth concls (j - 1) + more_consumes
-            in
-              Method.insert_tac (more_facts @ adefs) THEN'
-                (if simp then
-                   rotate_tac k (length adefs) THEN'
-                   arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
-                 else
-                   arbitrary_tac defs_ctxt k xs)
-             end)
-          THEN' inner_atomize_tac defs_ctxt) j))
-        THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
-            guess_instance ctxt (internalize ctxt more_consumes rule) i st'
-            |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
-            |> Seq.maps (fn rule' =>
-              CASES (rule_cases ctxt rule' cases)
-                (rtac rule' i THEN
-                  PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
-    THEN_ALL_NEW_CASES
-      ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac)
-        else K all_tac)
-       THEN_ALL_NEW rulify_tac ctxt)
-  end;
+  SUBGOAL_CASES (fn (_, i, st) =>
+    let
+      val thy = Proof_Context.theory_of ctxt;
+  
+      val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
+      val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
+  
+      fun inst_rule (concls, r) =
+        (if null insts then `Rule_Cases.get r
+         else (align_left "Rule has fewer conclusions than arguments given"
+            (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
+          |> maps (prep_inst ctxt align_right (atomize_term thy))
+          |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
+        |> mod_cases thy
+        |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
+  
+      val ruleq =
+        (case opt_rule of
+          SOME rs => Seq.single (inst_rule (Rule_Cases.strict_mutual_rule ctxt rs))
+        | NONE =>
+            (get_inductP ctxt facts @
+              map (special_rename_params defs_ctxt insts) (get_inductT ctxt insts))
+            |> map_filter (Rule_Cases.mutual_rule ctxt)
+            |> tap (trace_rules ctxt inductN o map #2)
+            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
+  
+      fun rule_cases ctxt rule cases =
+        let
+          val rule' = Rule_Cases.internalize_params rule;
+          val rule'' = rule' |> simp ? simplified_rule ctxt;
+          val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
+          val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
+        in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') cases' end;
+    in
+      fn st =>
+        ruleq
+        |> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
+        |> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
+          (PRECISE_CONJUNCTS (length concls) (ALLGOALS (fn j =>
+            (CONJUNCTS (ALLGOALS
+              let
+                val adefs = nth_list atomized_defs (j - 1);
+                val frees = fold (Term.add_frees o Thm.prop_of) adefs [];
+                val xs = nth_list arbitrary (j - 1);
+                val k = nth concls (j - 1) + more_consumes
+              in
+                Method.insert_tac (more_facts @ adefs) THEN'
+                  (if simp then
+                     rotate_tac k (length adefs) THEN'
+                     arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
+                   else
+                     arbitrary_tac defs_ctxt k xs)
+               end)
+            THEN' inner_atomize_tac defs_ctxt) j))
+          THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
+              guess_instance ctxt (internalize ctxt more_consumes rule) i st'
+              |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
+              |> Seq.maps (fn rule' =>
+                CASES (rule_cases ctxt rule' cases)
+                  (rtac rule' i THEN
+                    PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))
+      end)
+      THEN_ALL_NEW_CASES
+        ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac) else K all_tac)
+         THEN_ALL_NEW rulify_tac ctxt);
 
 val induct_tac = gen_induct_tac (K I);
 
@@ -832,7 +832,7 @@
 
 in
 
-fun coinduct_tac ctxt inst taking opt_rule facts =
+fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i, st) =>
   let
     val thy = Proof_Context.theory_of ctxt;
 
@@ -849,7 +849,7 @@
           |> tap (trace_rules ctxt coinductN)
           |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   in
-    SUBGOAL_CASES (fn (goal, i) => fn st =>
+    fn st =>
       ruleq goal
       |> Seq.maps (Rule_Cases.consume ctxt [] facts)
       |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
@@ -858,8 +858,8 @@
         |> Seq.maps (fn rule' =>
           CASES (Rule_Cases.make_common (thy,
               Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
-            (Method.insert_tac more_facts i THEN rtac rule' i) st)))
-  end;
+            (Method.insert_tac more_facts i THEN rtac rule' i) st))
+  end);
 
 end;
 
diff -r 67a5f004583d -r 713ae0c9e652 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Thu Mar 20 15:13:55 2014 -0700
+++ b/src/ZF/Tools/induct_tacs.ML	Thu Mar 20 23:38:34 2014 +0100
@@ -89,7 +89,7 @@
       (2) exhaustion works for VARIABLES in the premises, not general terms
 **)
 
-fun exhaust_induct_tac exh ctxt var i state =
+fun exhaust_induct_tac exh ctxt var i state = SUBGOAL (fn _ =>
   let
     val thy = Proof_Context.theory_of ctxt
     val ({context = ctxt', asms, ...}, _) = Subgoal.focus ctxt i state
@@ -102,12 +102,12 @@
              [] => error "induction is not available for this datatype"
            | major::_ => FOLogic.dest_Trueprop major)
   in
-    eres_inst_tac ctxt [(ixn, var)] rule i state
+    eres_inst_tac ctxt [(ixn, var)] rule i
   end
   handle Find_tname msg =>
             if exh then (*try boolean case analysis instead*)
-                case_tac ctxt var i state
-            else error msg;
+                case_tac ctxt var i
+            else error msg) i state;
 
 val exhaust_tac = exhaust_induct_tac true;
 val induct_tac = exhaust_induct_tac false;