# HG changeset patch
# User wenzelm
# Date 1428524103 -7200
# Node ID 8a53364a3143f08cb6a268c2d1503a6de2265bcc
# Parent  2fcf41a626f7c296ce30299e0113834114299e38# Parent  c2dc7856e2e582d13ce04eb211be9009161e8e59
merged

diff -r 2fcf41a626f7 -r 8a53364a3143 etc/symbols
--- a/etc/symbols	Wed Apr 08 19:24:32 2015 +0200
+++ b/etc/symbols	Wed Apr 08 22:15:03 2015 +0200
@@ -347,6 +347,7 @@
 \<cedilla>              code: 0x0000b8
 \<hungarumlaut>         code: 0x0002dd
 \<some>                 code: 0x0003f5
+\<hole>                 code: 0x002311
 \<newline>              code: 0x0023ce
 \<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
 \<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
@@ -358,4 +359,3 @@
 \<^esub>                code: 0x0021d9  group: control_block  font: IsabelleText  abbrev: =_)
 \<^bsup>                code: 0x0021d7  group: control_block  font: IsabelleText  abbrev: =^(
 \<^esup>                code: 0x0021d6  group: control_block  font: IsabelleText  abbrev: =^)
-
diff -r 2fcf41a626f7 -r 8a53364a3143 lib/fonts/IsabelleText.sfd
--- a/lib/fonts/IsabelleText.sfd	Wed Apr 08 19:24:32 2015 +0200
+++ b/lib/fonts/IsabelleText.sfd	Wed Apr 08 22:15:03 2015 +0200
@@ -19,7 +19,7 @@
 OS2_WeightWidthSlopeOnly: 0
 OS2_UseTypoMetrics: 1
 CreationTime: 1050361371
-ModificationTime: 1392668982
+ModificationTime: 1428519538
 PfmFamily: 17
 TTFWeight: 400
 TTFWidth: 5
@@ -2242,7 +2242,7 @@
 FitToEm: 1
 WinInfo: 8912 16 10
 TeXData: 1 0 0 631296 315648 210432 572416 -1048576 210432 783286 444596 497025 792723 393216 433062 380633 303038 157286 324010 404750 52429 2506097 1059062 262144
-BeginChars: 1114189 1096
+BeginChars: 1114189 1097
 
 StartChar: u10000
 Encoding: 65536 65536 0
@@ -55594,5 +55594,25 @@
  268.5 122 l 17,5,-1
 EndSplineSet
 EndChar
+
+StartChar: uni2311
+Encoding: 8977 8977 1096
+Width: 1233
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+231 394 m 1,0,1
+ 616 531 616 531 1001 394 c 1,2,3
+ 864 778 864 778 1001 1164 c 1,4,5
+ 616 1026 616 1026 231 1164 c 1,6,7
+ 368 778 368 778 231 394 c 1,0,1
+97 258 m 1,8,9
+ 281 758 281 758 97 1298 c 1,10,11
+ 616 1121 616 1121 1136 1298 c 1,12,13
+ 952 798 952 798 1136 259 c 1,14,15
+ 616 436 616 436 97 258 c 1,8,9
+EndSplineSet
+EndChar
 EndChars
 EndSplineFont
diff -r 2fcf41a626f7 -r 8a53364a3143 lib/fonts/IsabelleText.ttf
Binary file lib/fonts/IsabelleText.ttf has changed
diff -r 2fcf41a626f7 -r 8a53364a3143 lib/fonts/IsabelleTextBold.sfd
--- a/lib/fonts/IsabelleTextBold.sfd	Wed Apr 08 19:24:32 2015 +0200
+++ b/lib/fonts/IsabelleTextBold.sfd	Wed Apr 08 22:15:03 2015 +0200
@@ -19,7 +19,7 @@
 OS2_WeightWidthSlopeOnly: 0
 OS2_UseTypoMetrics: 1
 CreationTime: 1050374980
-ModificationTime: 1392669044
+ModificationTime: 1428519645
 PfmFamily: 17
 TTFWeight: 700
 TTFWidth: 5
@@ -1675,7 +1675,7 @@
 AntiAlias: 1
 FitToEm: 1
 WinInfo: 8928 16 10
-BeginChars: 1114112 1085
+BeginChars: 1114112 1086
 
 StartChar: u10000
 Encoding: 65536 65536 0
@@ -58524,5 +58524,25 @@
  298 187 l 17,5,-1
 EndSplineSet
 EndChar
+
+StartChar: uni2311
+Encoding: 8977 8977 1085
+Width: 1233
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+250 412 m 1,0,1
+ 616 544 616 544 982 412 c 1,2,3
+ 851 778 851 778 982 1144 c 1,4,5
+ 616 1014 616 1014 250 1144 c 1,6,7
+ 381 778 381 778 250 412 c 1,0,1
+71 232 m 1,8,9
+ 264 756 264 756 71 1324 c 1,10,11
+ 616 1138 616 1138 1162 1324 c 1,12,13
+ 969 800 969 800 1162 234 c 1,14,15
+ 617 418 617 418 71 232 c 1,8,9
+EndSplineSet
+EndChar
 EndChars
 EndSplineFont
diff -r 2fcf41a626f7 -r 8a53364a3143 lib/fonts/IsabelleTextBold.ttf
Binary file lib/fonts/IsabelleTextBold.ttf has changed
diff -r 2fcf41a626f7 -r 8a53364a3143 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Wed Apr 08 19:24:32 2015 +0200
+++ b/lib/texinputs/isabellesym.sty	Wed Apr 08 22:15:03 2015 +0200
@@ -356,5 +356,5 @@
 \newcommand{\isasymsome}{\isamath{\epsilon\,}}
 \newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}
 \newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
+\newcommand{\isasymhole}{\isatext{\rm\wasylozenge}}  %requires wasysym
 \newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
-
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Doc/Isar_Ref/document/root.tex
--- a/src/Doc/Isar_Ref/document/root.tex	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Doc/Isar_Ref/document/root.tex	Wed Apr 08 22:15:03 2015 +0200
@@ -1,6 +1,7 @@
 \documentclass[12pt,a4paper,fleqn]{report}
 \usepackage[T1]{fontenc}
 \usepackage{amssymb}
+\usepackage{wasysym}
 \usepackage{eurosym}
 \usepackage[english]{babel}
 \usepackage[only,bigsqcap]{stmaryrd}
diff -r 2fcf41a626f7 -r 8a53364a3143 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/FOL/simpdata.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -88,7 +88,7 @@
 
 structure Splitter = Splitter
 (
-  val thy = @{theory}
+  val context = @{context}
   val mk_eq = mk_eq
   val meta_eq_to_iff = @{thm meta_eq_to_iff}
   val iffD = @{thm iffD2}
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Decision_Procs/approximation.ML
--- a/src/HOL/Decision_Procs/approximation.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -50,7 +50,7 @@
 
 (* Should be in HOL.thy ? *)
 fun gen_eval_tac conv ctxt = CONVERSION
-  (Object_Logic.judgment_conv (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt))
+  (Object_Logic.judgment_conv ctxt (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt))
   THEN' rtac TrueI
 
 val form_equations = @{thms interpret_form_equations};
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Decision_Procs/ferrante_rackoff.ML
--- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -226,7 +226,7 @@
   | SOME instance =>
       Object_Logic.full_atomize_tac ctxt i THEN
       simp_tac (put_simpset (#simpset (snd instance)) ctxt) i THEN  (* FIXME already part of raw_ferrack_qe_conv? *)
-      CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
+      CONVERSION (Object_Logic.judgment_conv ctxt (raw_ferrack_qe_conv ctxt instance)) i THEN
       simp_tac ctxt i));  (* FIXME really? *)
 
 end;
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Decision_Procs/langford.ML
--- a/src/HOL/Decision_Procs/langford.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Decision_Procs/langford.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -261,6 +261,6 @@
       THEN (CONVERSION Thm.eta_long_conversion) i
       THEN (TRY o generalize_tac (cfrees (#atoms instance))) i
       THEN Object_Logic.full_atomize_tac ctxt i
-      THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ctxt ss instance)) i
+      THEN CONVERSION (Object_Logic.judgment_conv ctxt (raw_dlo_conv ctxt ss instance)) i
       THEN (simp_tac (put_simpset ss ctxt) i)));
 end;
\ No newline at end of file
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/GCD.thy	Wed Apr 08 22:15:03 2015 +0200
@@ -49,8 +49,8 @@
 
 class semiring_gcd = comm_semiring_1 + gcd +
   assumes gcd_dvd1 [iff]: "gcd a b dvd a"
-		and gcd_dvd2 [iff]: "gcd a b dvd b"
-		and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b"
+    and gcd_dvd2 [iff]: "gcd a b dvd b"
+    and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b"
 
 class ring_gcd = comm_ring_1 + semiring_gcd
 
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/HOL.thy	Wed Apr 08 22:15:03 2015 +0200
@@ -848,7 +848,7 @@
 apply (rule prem)
 apply assumption
 apply (rule allI)+
-apply (tactic {* eresolve_tac @{context} [Classical.dup_elim NONE @{thm allE}] 1 *})
+apply (tactic {* eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1 *})
 apply iprover
 done
 
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Library/Rewrite.thy
--- a/src/HOL/Library/Rewrite.thy	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Library/Rewrite.thy	Wed Apr 08 22:15:03 2015 +0200
@@ -1,17 +1,22 @@
+(*  Title:      HOL/Library/Rewrite.thy
+    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
+
+Proof method "rewrite" with support for subterm-selection based on patterns.
+*)
+
 theory Rewrite
 imports Main
 begin
 
-consts rewrite_HOLE :: "'a :: {}"
+consts rewrite_HOLE :: "'a::{}"
 notation rewrite_HOLE ("HOLE")
 notation rewrite_HOLE ("\<box>")
 
 lemma eta_expand:
-  fixes f :: "'a :: {} \<Rightarrow> 'b :: {}" shows "f \<equiv> (\<lambda>x. f x)"
-  by (rule reflexive)
+  fixes f :: "'a::{} \<Rightarrow> 'b::{}"
+  shows "f \<equiv> \<lambda>x. f x" .
 
 ML_file "cconv.ML"
 ML_file "rewrite.ML"
-setup Rewrite.setup
 
 end
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Library/bnf_lfp_countable.ML
--- a/src/HOL/Library/bnf_lfp_countable.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Library/bnf_lfp_countable.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -172,7 +172,7 @@
       Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
         mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps'
           inj_map_strongs')
-      |> HOLogic.conj_elims
+      |> HOLogic.conj_elims ctxt
       |> Proof_Context.export names_ctxt ctxt
       |> map Thm.close_derivation
     end;
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Library/cconv.ML
--- a/src/HOL/Library/cconv.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Library/cconv.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -1,3 +1,9 @@
+(*  Title:      HOL/Library/cconv.ML
+    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
+
+FIXME!?
+*)
+
 infix 1 then_cconv
 infix 0 else_cconv
 
@@ -170,7 +176,8 @@
 fun prems_cconv 0 cv ct = cv ct
   | prems_cconv n cv ct =
       (case ct |> Thm.term_of of
-        (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
+        (Const (@{const_name "Pure.imp"}, _) $ _) $ _ =>
+          ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
       | _ =>  cv ct)
 
 (*rewrite B in A1 Pure.imp ... Pure.imp An Pure.imp B*)
@@ -212,7 +219,7 @@
       end
   | NONE => raise THM ("gconv_rule", i, [th]))
 
-  (* Conditional conversions as tactics. *)
+(* Conditional conversions as tactics. *)
 fun CCONVERSION cv i st = Seq.single (gconv_rule cv i st)
   handle THM _ => Seq.empty
        | CTERM _ => Seq.empty
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Library/rewrite.ML
--- a/src/HOL/Library/rewrite.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Library/rewrite.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -1,24 +1,26 @@
-(* Author: Christoph Traut, Lars Noschinski
+(*  Title:      HOL/Library/rewrite.ML
+    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
 
-  This is a rewrite method supports subterm-selection based on patterns.
+This is a rewrite method that supports subterm-selection based on patterns.
 
-  The patterns accepted by rewrite are of the following form:
-    <atom>    ::= <term> | "concl" | "asm" | "for" "(" <names> ")"
-    <pattern> ::= (in <atom> | at <atom>) [<pattern>]
-    <args>    ::= [<pattern>] ("to" <term>) <thms>
+The patterns accepted by rewrite are of the following form:
+  <atom>    ::= <term> | "concl" | "asm" | "for" "(" <names> ")"
+  <pattern> ::= (in <atom> | at <atom>) [<pattern>]
+  <args>    ::= [<pattern>] ("to" <term>) <thms>
 
-  This syntax was clearly inspired by Gonthier's and Tassi's language of
-  patterns but has diverged significantly during its development.
+This syntax was clearly inspired by Gonthier's and Tassi's language of
+patterns but has diverged significantly during its development.
 
-  We also allow introduction of identifiers for bound variables,
-  which can then be used to match arbitary subterms inside abstractions.
+We also allow introduction of identifiers for bound variables,
+which can then be used to match arbitrary subterms inside abstractions.
 *)
 
-signature REWRITE1 = sig
-  val setup : theory -> theory
+signature REWRITE =
+sig
+  (* FIXME proper ML interface!? *)
 end
 
-structure Rewrite : REWRITE1 =
+structure Rewrite : REWRITE =
 struct
 
 datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list
@@ -68,8 +70,10 @@
   let
     fun add_ident NONE _ l = l
       | add_ident (SOME name) ct l = (name, Thm.term_of ct) :: l
-    fun inner rewr ctxt idents = CConv.abs_cconv (fn (ct, ctxt) => rewr ctxt (add_ident ident ct idents)) ctxt
+    fun inner rewr ctxt idents =
+      CConv.abs_cconv (fn (ct, ctxt) => rewr ctxt (add_ident ident ct idents)) ctxt
   in inner end
+
 val fun_rewr_cconv : subterm_position = fn rewr => CConv.fun_cconv oo rewr
 val arg_rewr_cconv : subterm_position = fn rewr => CConv.arg_cconv oo rewr
 
@@ -80,17 +84,19 @@
   case try (fastype_of #> dest_funT) u of
     NONE => raise TERM ("ft_abs: no function type", [u])
   | SOME (U, _) =>
-  let
-    val tyenv' = if T = dummyT then tyenv else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv
-    val x = Free (the_default (Name.internal dummyN) s, Envir.norm_type tyenv' T)
-    val eta_expand_cconv = CConv.rewr_cconv @{thm eta_expand}
-    fun eta_expand rewr ctxt bounds = eta_expand_cconv then_conv rewr ctxt bounds
-    val (u', pos') =
-      case u of
-        Abs (_,_,t') => (subst_bound (x, t'), pos o abs_rewr_cconv s)
-      | _ => (u $ x, pos o eta_expand o abs_rewr_cconv s)
-  in (tyenv', u', pos') end
-  handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u])
+      let
+        val tyenv' =
+          if T = dummyT then tyenv
+          else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv
+        val x = Free (the_default (Name.internal dummyN) s, Envir.norm_type tyenv' T)
+        val eta_expand_cconv = CConv.rewr_cconv @{thm eta_expand}
+        fun eta_expand rewr ctxt bounds = eta_expand_cconv then_conv rewr ctxt bounds
+        val (u', pos') =
+          case u of
+            Abs (_,_,t') => (subst_bound (x, t'), pos o abs_rewr_cconv s)
+          | _ => (u $ x, pos o eta_expand o abs_rewr_cconv s)
+      in (tyenv', u', pos') end
+      handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u])
 
 fun ft_fun _ (tyenv, l $ _, pos) = (tyenv, l, pos o fun_rewr_cconv)
   | ft_fun ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_fun ctxt o ft_abs ctxt (NONE, T)) ft
@@ -127,7 +133,8 @@
           | (x :: xs) => (xs , desc o ft_all ctxt x)
         end
       | f rev_idents _ = (rev_idents, I)
-  in case f (rev idents) t of
+  in
+    case f (rev idents) t of
       ([], ft') => SOME (ft' ft)
     | _ => NONE
   end
@@ -143,7 +150,7 @@
   | _ => raise TERM ("ft_assm", [t])
 
 fun ft_judgment ctxt (ft as (_, t, _) : focusterm) =
-  if Object_Logic.is_judgment (Proof_Context.theory_of ctxt) t
+  if Object_Logic.is_judgment ctxt t
   then ft_arg ctxt ft
   else ft
 
@@ -153,7 +160,8 @@
 fun find_subterms ctxt condition (ft as (_, t, _) : focusterm) =
   let
     val recurse = find_subterms ctxt condition
-    val recursive_matches = case t of
+    val recursive_matches =
+      case t of
         _ $ _ => Seq.append (ft |> ft_fun ctxt |> recurse) (ft |> ft_arg ctxt |> recurse)
       | Abs (_,T,_) => ft |> ft_abs ctxt (NONE, T) |> recurse
       | _ => Seq.empty
@@ -250,7 +258,6 @@
     fun apply_pats ft = ft
       |> Seq.single
       |> fold apply_pat pattern_list
-
   in
     apply_pats
   end
@@ -322,9 +329,9 @@
     val tac = rewrite_goal_with_thm ctxt pattern thms'
   in tac end
 
-val setup =
+val _ =
+  Theory.setup
   let
-
     fun mk_fix s = (Binding.name s, NONE, NoSyn)
 
     val raw_pattern : (string, binding * string option * mixfix) pattern list parser =
@@ -342,11 +349,11 @@
 
       in Scan.repeat sep_atom >> (flat #> rev #> append_default) end
 
-    fun ctxt_lift (scan : 'a parser) f = fn (ctxt : Context.generic, toks) =>
+    fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) =>
       let
         val (r, toks') = scan toks
-        val (r', ctxt') = Context.map_proof_result (fn ctxt => f ctxt r) ctxt
-      in (r', (ctxt', toks' : Token.T list))end
+        val (r', context') = Context.map_proof_result (fn ctxt => f ctxt r) context
+      in (r', (context', toks' : Token.T list)) end
 
     fun read_fixes fixes ctxt =
       let fun read_typ (b, rawT, mx) = (b, Option.map (Syntax.read_typ ctxt) rawT, mx)
@@ -354,7 +361,6 @@
 
     fun prep_pats ctxt (ps : (string, binding * string option * mixfix) pattern list) =
       let
-
         fun add_constrs ctxt n (Abs (x, T, t)) =
             let
               val (x', ctxt') = yield_singleton Proof_Context.add_fixes (mk_fix x) ctxt
@@ -470,10 +476,11 @@
 
     val subst_parser =
       let val scan = raw_pattern -- to_parser -- Parse.xthms1
-      in ctxt_lift scan prep_args end
+      in context_lift scan prep_args end
   in
     Method.setup @{binding rewrite} (subst_parser >>
-      (fn (pattern, inthms, inst) => fn ctxt => SIMPLE_METHOD' (rewrite_tac ctxt (pattern, inst) inthms)))
+      (fn (pattern, inthms, inst) => fn ctxt =>
+        SIMPLE_METHOD' (rewrite_tac ctxt (pattern, inst) inthms)))
       "single-step rewriting, allowing subterm selection via patterns."
   end
 end
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -321,7 +321,7 @@
           Config.put Quickcheck.finite_types true #>
           Config.put Quickcheck.finite_type_size 1 #>
           Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
-        (false, false) [])) (map (rpair [] o Object_Logic.atomize_term thy)
+        (false, false) [])) (map (rpair [] o Object_Logic.atomize_term ctxt)
         (fst (Variable.import_terms true [t] ctxt)))
   end
 
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Nitpick_Examples/minipick.ML
--- a/src/HOL/Nitpick_Examples/minipick.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Nitpick_Examples/minipick.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -409,7 +409,7 @@
       | concrete (Type (@{type_name prod}, Ts)) = forall concrete Ts
       | concrete _ = true
     val neg_t =
-      @{const Not} $ Object_Logic.atomize_term thy t
+      @{const Not} $ Object_Logic.atomize_term ctxt t
       |> map_types unsetify_type
     val _ = fold_types (K o check_type ctxt raw_infinite) neg_t ()
     val frees = Term.add_frees neg_t []
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -93,7 +93,7 @@
 
     fun rule_cases ctxt r =
       let val r' = if simp then Induct.simplified_rule ctxt r else r
-      in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end;
+      in Rule_Cases.make_nested ctxt (Thm.prop_of r') (Induct.rulified_term ctxt r') end;
   in
     (fn i => fn st =>
       rules
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Probability/Giry_Monad.thy	Wed Apr 08 22:15:03 2015 +0200
@@ -324,7 +324,7 @@
   finally show ?thesis .
 qed
 
-(* TODO: Rename. This name is too general – Manuel *)
+(* TODO: Rename. This name is too general -- Manuel *)
 lemma measurable_pair_measure:
   assumes f: "f \<in> measurable M (subprob_algebra N)"
   assumes g: "g \<in> measurable M (subprob_algebra L)"
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/ROOT	Wed Apr 08 22:15:03 2015 +0200
@@ -31,6 +31,7 @@
   *}
   theories
     Library
+    Rewrite
     (*conflicting type class instantiations*)
     List_lexord
     Sublist_Order
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -1243,10 +1243,9 @@
 
 fun presimp_prop ctxt type_enc t =
   let
-    val thy = Proof_Context.theory_of ctxt
     val t = t |> Envir.beta_eta_contract
               |> transform_elim_prop
-              |> Object_Logic.atomize_term thy
+              |> Object_Logic.atomize_term ctxt
     val need_trueprop = (fastype_of t = @{typ bool})
     val is_ho = is_type_enc_higher_order type_enc
   in
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Tools/ATP/atp_waldmeister.ML
--- a/src/HOL/Tools/ATP/atp_waldmeister.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Tools/ATP/atp_waldmeister.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -445,7 +445,7 @@
   let
     val thy = Proof_Context.theory_of ctxt
 
-    val preproc = Object_Logic.atomize_term thy
+    val preproc = Object_Logic.atomize_term ctxt
 
     val conditions = map preproc hyps_t0
     val consequence = preproc concl_t0
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -188,14 +188,12 @@
 
 fun mk_ind_goal ctxt branches =
   let
-    val thy = Proof_Context.theory_of ctxt
-
     fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
       HOLogic.mk_Trueprop (list_comb (P, map Free xs))
       |> fold_rev (curry Logic.mk_implies) Cs
       |> fold_rev (Logic.all o Free) ws
       |> term_conv ctxt (ind_atomize ctxt)
-      |> Object_Logic.drop_judgment thy
+      |> Object_Logic.drop_judgment ctxt
       |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
   in
     Sum_Tree.mk_sumcases HOLogic.boolT (map brnch branches)
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Tools/Function/relation.ML
--- a/src/HOL/Tools/Function/relation.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Tools/Function/relation.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -10,40 +10,42 @@
   val relation_infer_tac: Proof.context -> term -> int -> tactic
 end
 
-structure Function_Relation : FUNCTION_RELATION =
+structure Function_Relation: FUNCTION_RELATION =
 struct
 
 (* tactic version *)
 
-fun inst_state_tac ctxt inst st =
-  (case Term.add_vars (Thm.prop_of st) [] of  (* FIXME tactic should not inspect main conclusion *)
-    [v as (_, T)] =>
-      PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt (inst T))])) st
-  | _ => Seq.empty);
+fun inst_state_tac ctxt inst =
+  SUBGOAL (fn (goal, _) =>
+    (case Term.add_vars goal [] of
+      [v as (_, T)] =>
+        PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt (inst T))]))
+    | _ => no_tac));
 
 fun relation_tac ctxt rel i =
   TRY (Function_Common.termination_rule_tac ctxt i)
-  THEN inst_state_tac ctxt rel;
+  THEN inst_state_tac ctxt rel i;
 
 
 (* version with type inference *)
 
-fun inst_state_infer_tac ctxt rel st =
-  (case Term.add_vars (Thm.prop_of st) [] of  (* FIXME tactic should not inspect main conclusion *)
-    [v as (_, T)] =>
-      let
-        val rel' = singleton (Variable.polymorphic ctxt) rel
-          |> map_types Type_Infer.paramify_vars
-          |> Type.constraint T
-          |> Syntax.check_term ctxt
-          |> Thm.cterm_of ctxt;
-      in
-        PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), rel')])) st
-      end
-  | _ => Seq.empty);
+fun inst_state_infer_tac ctxt rel =
+  SUBGOAL (fn (goal, _) =>
+    (case Term.add_vars goal [] of
+      [v as (_, T)] =>
+        let
+          val rel' =
+            singleton (Variable.polymorphic ctxt) rel
+            |> map_types Type_Infer.paramify_vars
+            |> Type.constraint T
+            |> Syntax.check_term ctxt;
+        in
+          PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt rel')]))
+        end
+    | _ => no_tac));
 
 fun relation_infer_tac ctxt rel i =
   TRY (Function_Common.termination_rule_tac ctxt i)
-  THEN inst_state_infer_tac ctxt rel;
+  THEN inst_state_infer_tac ctxt rel i;
 
 end
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -32,8 +32,6 @@
   val decompose_tac : Proof.context -> ttac
 end
 
-
-
 structure Termination : TERMINATION =
 struct
 
@@ -275,14 +273,13 @@
 
 fun wf_union_tac ctxt st = SUBGOAL (fn _ =>
   let
-    val thy = Proof_Context.theory_of ctxt
     val ((_ $ (_ $ rel)) :: ineqs) = Thm.prems_of st
 
     fun mk_compr ineq =
       let
         val (vars, prems, lhs, rhs) = dest_term ineq
       in
-        mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (Object_Logic.atomize_term thy) prems)
+        mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (Object_Logic.atomize_term ctxt) prems)
       end
 
     val relation =
@@ -360,5 +357,4 @@
     else solve_trivial_tac D i
   end)
 
-
 end
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -300,7 +300,7 @@
     val psimp_table = const_psimp_table ctxt subst
     val choice_spec_table = const_choice_spec_table ctxt subst
     val nondefs =
-      nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
+      nondefs |> filter_out (is_choice_spec_axiom ctxt choice_spec_table)
     val intro_table = inductive_intro_table ctxt subst def_tables
     val ground_thm_table = ground_theorem_table thy
     val ersatz_table = ersatz_table ctxt
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -218,7 +218,7 @@
   val nondef_props_for_const :
     theory -> bool -> const_table -> string * typ -> term list
   val is_choice_spec_fun : hol_context -> string * typ -> bool
-  val is_choice_spec_axiom : theory -> const_table -> term -> bool
+  val is_choice_spec_axiom : Proof.context -> const_table -> term -> bool
   val is_raw_equational_fun : hol_context -> string * typ -> bool
   val is_equational_fun : hol_context -> string * typ -> bool
   val codatatype_bisim_axioms : hol_context -> typ -> term list
@@ -1548,13 +1548,13 @@
   | unvarify_term (Abs (s, T, t')) = Abs (s, T, unvarify_term t')
   | unvarify_term t = t
 
-fun axiom_for_choice_spec thy =
+fun axiom_for_choice_spec ctxt =
   unvarify_term
-  #> Object_Logic.atomize_term thy
+  #> Object_Logic.atomize_term ctxt
   #> Choice_Specification.close_form
   #> HOLogic.mk_Trueprop
 
-fun is_choice_spec_fun ({thy, def_tables, nondef_table, choice_spec_table, ...}
+fun is_choice_spec_fun ({thy, ctxt, def_tables, nondef_table, choice_spec_table, ...}
                         : hol_context) x =
   case nondef_props_for_const thy true choice_spec_table x of
     [] => false
@@ -1565,7 +1565,7 @@
             let val ts' = nondef_props_for_const thy true nondef_table x in
               length ts' = length ts andalso
               forall (fn t =>
-                         exists (curry (op aconv) (axiom_for_choice_spec thy t))
+                         exists (curry (op aconv) (axiom_for_choice_spec ctxt t))
                                 ts') ts
             end
 
@@ -2074,10 +2074,10 @@
 
 exception NO_TRIPLE of unit
 
-fun triple_for_intro_rule thy x t =
+fun triple_for_intro_rule ctxt x t =
   let
-    val prems = Logic.strip_imp_prems t |> map (Object_Logic.atomize_term thy)
-    val concl = Logic.strip_imp_concl t |> Object_Logic.atomize_term thy
+    val prems = Logic.strip_imp_prems t |> map (Object_Logic.atomize_term ctxt)
+    val concl = Logic.strip_imp_concl t |> Object_Logic.atomize_term ctxt
     val (main, side) = List.partition (exists_Const (curry (op =) x)) prems
     val is_good_head = curry (op =) (Const x) o head_of
   in
@@ -2122,7 +2122,7 @@
     [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
                       [Const x])
   | intro_ts =>
-    (case map (triple_for_intro_rule thy x) intro_ts
+    (case map (triple_for_intro_rule ctxt x) intro_ts
           |> filter_out (null o #2) of
        [] => true
      | triples =>
@@ -2149,7 +2149,7 @@
            SOME wf => wf
          | NONE =>
            let
-             val goal = prop |> Thm.global_cterm_of thy |> Goal.init
+             val goal = prop |> Thm.cterm_of ctxt |> Goal.init
              val wf = exists (terminates_by ctxt tac_timeout goal)
                              termination_tacs
            in Synchronized.change cached_wf_props (cons (prop, wf)); wf end
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -1050,7 +1050,7 @@
     fun try_out negate =
       let
         val concl = (negate ? curry (op $) @{const Not})
-                    (Object_Logic.atomize_term thy prop)
+                    (Object_Logic.atomize_term ctxt prop)
         val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl))
                    |> map_types (map_type_tfree
                                      (fn (s, []) => TFree (s, @{sort type})
@@ -1062,7 +1062,7 @@
             |> writeln
           else
             ()
-        val goal = prop |> Thm.global_cterm_of thy |> Goal.init
+        val goal = prop |> Thm.cterm_of ctxt |> Goal.init
       in
         (goal |> SINGLE (DETERM_TIMEOUT auto_timeout (auto_tac ctxt))
               |> the |> Goal.finish ctxt; true)
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Tools/Quickcheck/quickcheck_common.ML
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -236,7 +236,7 @@
     val rewrs = map (swap o dest) @{thms all_simps} @
       (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff},
         @{thm bot_fun_def}, @{thm less_bool_def}])
-    val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term thy t)
+    val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term ctxt t)
     val (vs, body) = strip_all t'
     val vs' = Variable.variant_frees ctxt [t'] vs
   in
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Tools/SMT/smtlib_isar.ML
--- a/src/HOL/Tools/SMT/smtlib_isar.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Tools/SMT/smtlib_isar.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -44,7 +44,7 @@
 fun postprocess_step_conclusion ctxt rewrite_rules ll_defs =
   let val thy = Proof_Context.theory_of ctxt in
     Raw_Simplifier.rewrite_term thy rewrite_rules []
-    #> Object_Logic.atomize_term thy
+    #> Object_Logic.atomize_term ctxt
     #> not (null ll_defs) ? unlift_term ll_defs
     #> simplify_bool
     #> unskolemize_names ctxt
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -428,10 +428,9 @@
 fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
   if Config.get ctxt instantiate_inducts then
     let
-      val thy = Proof_Context.theory_of ctxt
       val ind_stmt =
         (hyp_ts |> filter_out (null o external_frees), concl_t)
-        |> Logic.list_implies |> Object_Logic.atomize_term thy
+        |> Logic.list_implies |> Object_Logic.atomize_term ctxt
       val ind_stmt_xs = external_frees ind_stmt
     in
       maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Tools/coinduction.ML
--- a/src/HOL/Tools/coinduction.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Tools/coinduction.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -37,7 +37,7 @@
     (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o eresolve0_tac [thin_rl])) i st
   end;
 
-fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _, _) =>
+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 =
@@ -98,9 +98,9 @@
                DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
                  (case prems of
                    [] => all_tac
-                 | inv::case_prems =>
+                 | inv :: case_prems =>
                      let
-                       val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
+                       val (init, last) = funpow_yield (p + e - 1) (HOLogic.conj_elim ctxt) inv;
                        val inv_thms = init @ [last];
                        val eqs = take e inv_thms;
                        fun is_local_var t =
@@ -115,7 +115,7 @@
         end) ctxt) THEN'
       K (prune_params_tac ctxt))
     #> Seq.maps (fn st =>
-      CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, Thm.prop_of st) cases) all_tac st)
+      CASES (Rule_Cases.make_common ctxt (Thm.prop_of st) cases) all_tac st)
   end));
 
 local
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Tools/groebner.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -677,13 +677,13 @@
 fun refute ctxt tm =
  if tm aconvc false_tm then assume_Trueprop tm else
  ((let
-   val (nths0,eths0) = List.partition (is_neg o concl) (HOLogic.conj_elims (assume_Trueprop tm))
+   val (nths0,eths0) = List.partition (is_neg o concl) (HOLogic.conj_elims ctxt (assume_Trueprop tm))
    val  nths = filter (is_eq o Thm.dest_arg o concl) nths0
    val eths = filter (is_eq o concl) eths0
   in
    if null eths then
     let
-      val th1 = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr th1 th2)) nths
+      val th1 = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr ctxt th1 th2)) nths
       val th2 =
         Conv.fconv_rule
           ((Conv.arg_conv #> Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) th1
@@ -703,13 +703,13 @@
       end
      else
       let
-       val nth = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr th1 th2)) nths
+       val nth = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr ctxt th1 th2)) nths
        val (vars,pol::pols) =
           grobify_equations(list_mk_conj(Thm.dest_arg(concl nth)::map concl eths))
        val (deg,l,cert) = grobner_strong vars pols pol
        val th1 =
         Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) nth
-       val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr th1) neq_01
+       val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr ctxt th1) neq_01
       in (vars,l,cert,th2)
       end)
     val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c >/ rat_0) p)) cert
@@ -724,7 +724,7 @@
               (nth eths i |> mk_meta_eq)) pols)
     val th1 = thm_fn herts_pos
     val th2 = thm_fn herts_neg
-    val th3 = HOLogic.conj_intr(mk_add (Thm.symmetric th1) th2 |> mk_object_eq) noteqth
+    val th3 = HOLogic.conj_intr ctxt (mk_add (Thm.symmetric th1) th2 |> mk_object_eq) noteqth
     val th4 =
       Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv o Conv.binop_conv) ring_normalize_conv)
         (neq_rule l th3)
@@ -931,7 +931,7 @@
   Object_Logic.full_atomize_tac ctxt
   THEN' presimplify ctxt add_ths del_ths
   THEN' CSUBGOAL (fn (p, i) =>
-    rtac (let val form = Object_Logic.dest_judgment p
+    rtac (let val form = Object_Logic.dest_judgment ctxt p
           in case get_ring_ideal_convs ctxt form of
            NONE => Thm.reflexive form
           | SOME thy => #ring_conv thy ctxt form
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Tools/hologic.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -24,9 +24,9 @@
   val mk_set: typ -> term list -> term
   val dest_set: term -> term list
   val mk_UNIV: typ -> term
-  val conj_intr: thm -> thm -> thm
-  val conj_elim: thm -> thm * thm
-  val conj_elims: thm -> thm list
+  val conj_intr: Proof.context -> thm -> thm -> thm
+  val conj_elim: Proof.context -> thm -> thm * thm
+  val conj_elims: Proof.context -> thm -> thm list
   val conj: term
   val disj: term
   val imp: term
@@ -203,25 +203,25 @@
   | _ => raise CTERM ("Trueprop_conv", [ct]))
 
 
-fun conj_intr thP thQ =
+fun conj_intr ctxt thP thQ =
   let
-    val (P, Q) = apply2 (Object_Logic.dest_judgment o Thm.cprop_of) (thP, thQ)
+    val (P, Q) = apply2 (Object_Logic.dest_judgment ctxt o Thm.cprop_of) (thP, thQ)
       handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
     val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
   in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end;
 
-fun conj_elim thPQ =
+fun conj_elim ctxt thPQ =
   let
-    val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment (Thm.cprop_of thPQ))
+    val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment ctxt (Thm.cprop_of thPQ))
       handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
     val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
     val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ;
     val thQ = Thm.implies_elim (inst @{thm conjunct2}) thPQ;
   in (thP, thQ) end;
 
-fun conj_elims th =
-  let val (th1, th2) = conj_elim th
-  in conj_elims th1 @ conj_elims th2 end handle THM _ => [th];
+fun conj_elims ctxt th =
+  let val (th1, th2) = conj_elim ctxt th
+  in conj_elims ctxt th1 @ conj_elims ctxt th2 end handle THM _ => [th];
 
 val conj = @{term HOL.conj}
 and disj = @{term HOL.disj}
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Tools/simpdata.ML
--- a/src/HOL/Tools/simpdata.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Tools/simpdata.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -147,7 +147,7 @@
 
 structure Splitter = Splitter
 (
-  val thy = @{theory}
+  val context = @{context}
   val mk_eq = mk_eq
   val meta_eq_to_iff = @{thm meta_eq_to_obj_eq}
   val iffD = @{thm iffD2}
diff -r 2fcf41a626f7 -r 8a53364a3143 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy	Wed Apr 08 22:15:03 2015 +0200
@@ -443,23 +443,22 @@
 qed
 
 ML {*
-  fun eventually_elim_tac ctxt thms = SUBGOAL_CASES (fn (_, _, st) =>
+  fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
     let
-      val thy = Proof_Context.theory_of ctxt
-      val mp_thms = thms RL [@{thm eventually_rev_mp}]
+      val mp_thms = facts RL @{thms eventually_rev_mp}
       val raw_elim_thm =
         (@{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 = Thm.prop_of (raw_elim_thm RS st)
-      val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])])
+        |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
+      val cases_prop = Thm.prop_of (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal))
+      val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
     in
-      CASES cases (rtac raw_elim_thm 1)
-    end) 1
+      CASES cases (rtac raw_elim_thm i)
+    end)
 *}
 
 method_setup eventually_elim = {*
-  Scan.succeed (fn ctxt => METHOD_CASES (eventually_elim_tac ctxt))
+  Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
 *} "elimination of eventually quantifiers"
 
 
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Provers/classical.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -72,7 +72,7 @@
   val deepen_tac: Proof.context -> int -> int -> tactic
 
   val contr_tac: Proof.context -> int -> tactic
-  val dup_elim: Context.generic option -> thm -> thm
+  val dup_elim: Proof.context -> thm -> thm
   val dup_intr: thm -> thm
   val dup_step_tac: Proof.context -> int -> tactic
   val eq_mp_tac: Proof.context -> int -> tactic
@@ -96,7 +96,7 @@
 signature CLASSICAL =
 sig
   include BASIC_CLASSICAL
-  val classical_rule: thm -> thm
+  val classical_rule: Proof.context -> thm -> thm
   type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net
   val rep_cs: claset ->
    {safeIs: thm Item_Net.T,
@@ -144,8 +144,8 @@
     [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W
 *)
 
-fun classical_rule rule =
-  if is_some (Object_Logic.elim_concl rule) then
+fun classical_rule ctxt rule =
+  if is_some (Object_Logic.elim_concl ctxt rule) then
     let
       val rule' = rule RS Data.classical;
       val concl' = Thm.concl_of rule';
@@ -165,13 +165,8 @@
   else rule;
 
 (*flatten nested meta connectives in prems*)
-fun flat_rule opt_context th =
-  let
-    val ctxt =
-      (case opt_context of
-        NONE => Proof_Context.init_global (Thm.theory_of_thm th)
-      | SOME context => Context.proof_of context);
-  in Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt)) th end;
+fun flat_rule ctxt =
+  Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt));
 
 
 (*** Useful tactics for classical reasoning ***)
@@ -206,13 +201,8 @@
 (*Duplication of hazardous rules, for complete provers*)
 fun dup_intr th = zero_var_indexes (th RS Data.classical);
 
-fun dup_elim context th =
-  let
-    val ctxt =
-      (case context of
-        SOME c => Context.proof_of c
-      | NONE => Proof_Context.init_global (Thm.theory_of_thm th));
-    val rl = (th RSN (2, revcut_rl)) |> Thm.assumption (SOME ctxt) 2 |> Seq.hd;
+fun dup_elim ctxt th =
+  let val rl = (th RSN (2, revcut_rl)) |> Thm.assumption (SOME ctxt) 2 |> Seq.hd;
   in rule_by_tactic ctxt (TRYALL (eresolve_tac ctxt [revcut_rl])) rl end;
 
 
@@ -259,6 +249,9 @@
     In case of overlap, new rules are tried BEFORE old ones!!
 ***)
 
+fun default_context (SOME context) _ = Context.proof_of context
+  | default_context NONE th = Proof_Context.init_global (Thm.theory_of_thm th);
+
 (*For use with biresolve_tac.  Combines intro rules with swap to handle negated
   assumptions.  Pairs elim rules with true. *)
 fun joinrules (intrs, elims) =
@@ -320,7 +313,8 @@
   if warn_rules context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
   else
     let
-      val th' = flat_rule context th;
+      val ctxt = default_context context th;
+      val th' = flat_rule ctxt th;
       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
         List.partition Thm.no_prems [th'];
       val nI = Item_Net.length safeIs + 1;
@@ -349,7 +343,8 @@
     error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
   else
     let
-      val th' = classical_rule (flat_rule context th);
+      val ctxt = default_context context th;
+      val th' = classical_rule ctxt (flat_rule ctxt th);
       val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
         List.partition (fn rl => Thm.nprems_of rl=1) [th'];
       val nI = Item_Net.length safeIs;
@@ -381,7 +376,8 @@
   if warn_rules context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
   else
     let
-      val th' = flat_rule context th;
+      val ctxt = default_context context th;
+      val th' = flat_rule ctxt th;
       val nI = Item_Net.length hazIs + 1;
       val nE = Item_Net.length hazEs;
       val _ = warn_claset context th cs;
@@ -410,7 +406,8 @@
     error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
   else
     let
-      val th' = classical_rule (flat_rule context th);
+      val ctxt = default_context context th;
+      val th' = classical_rule ctxt (flat_rule ctxt th);
       val nI = Item_Net.length hazIs;
       val nE = Item_Net.length hazEs + 1;
       val _ = warn_claset context th cs;
@@ -418,7 +415,7 @@
       CS
        {hazEs = Item_Net.update th hazEs,
         haz_netpair = insert (nI, nE) ([], [th']) haz_netpair,
-        dup_netpair = insert (nI, nE) ([], [dup_elim context th']) dup_netpair,
+        dup_netpair = insert (nI, nE) ([], [dup_elim ctxt th']) dup_netpair,
         safeIs = safeIs,
         safeEs = safeEs,
         hazIs = hazIs,
@@ -443,7 +440,8 @@
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   if Item_Net.member safeIs th then
     let
-      val th' = flat_rule context th;
+      val ctxt = default_context context th;
+      val th' = flat_rule ctxt th;
       val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'];
     in
       CS
@@ -466,7 +464,8 @@
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   if Item_Net.member safeEs th then
     let
-      val th' = classical_rule (flat_rule context th);
+      val ctxt = default_context context th;
+      val th' = classical_rule ctxt (flat_rule ctxt th);
       val (safe0_rls, safep_rls) = List.partition (fn rl => Thm.nprems_of rl = 1) [th'];
     in
       CS
@@ -488,7 +487,10 @@
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   if Item_Net.member hazIs th then
-    let val th' = flat_rule context th in
+    let
+      val ctxt = default_context context th;
+      val th' = flat_rule ctxt th;
+    in
       CS
        {haz_netpair = delete ([th'], []) haz_netpair,
         dup_netpair = delete ([dup_intr th'], []) dup_netpair,
@@ -510,10 +512,13 @@
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
   if Item_Net.member hazEs th then
-    let val th' = classical_rule (flat_rule context th) in
+    let
+      val ctxt = default_context context th;
+      val th' = classical_rule ctxt (flat_rule ctxt th);
+    in
       CS
        {haz_netpair = delete ([], [th']) haz_netpair,
-        dup_netpair = delete ([], [dup_elim context th']) dup_netpair,
+        dup_netpair = delete ([], [dup_elim ctxt th']) dup_netpair,
         safeIs = safeIs,
         safeEs = safeEs,
         hazIs = hazIs,
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Provers/splitter.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -9,7 +9,7 @@
 
 signature SPLITTER_DATA =
 sig
-  val thy           : theory
+  val context       : Proof.context
   val mk_eq         : thm -> thm
   val meta_eq_to_iff: thm (* "x == y ==> x = y"                      *)
   val iffD          : thm (* "[| P = Q; Q |] ==> P"                  *)
@@ -43,14 +43,14 @@
 struct
 
 val Const (const_not, _) $ _ =
-  Object_Logic.drop_judgment Data.thy
+  Object_Logic.drop_judgment Data.context
     (#1 (Logic.dest_implies (Thm.prop_of Data.notnotD)));
 
 val Const (const_or , _) $ _ $ _ =
-  Object_Logic.drop_judgment Data.thy
+  Object_Logic.drop_judgment Data.context
     (#1 (Logic.dest_implies (Thm.prop_of Data.disjE)));
 
-val const_Trueprop = Object_Logic.judgment_name Data.thy;
+val const_Trueprop = Object_Logic.judgment_name Data.context;
 
 
 fun split_format_err () = error "Wrong format for split rule";
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -9,8 +9,8 @@
   val thesisN: string
   val thisN: string
   val assmsN: string
-  val goal: theory -> term list -> (indexname * term option) list
-  val facts: theory -> term list -> (indexname * term option) list
+  val goal: Proof.context -> term list -> (indexname * term option) list
+  val facts: Proof.context -> term list -> (indexname * term option) list
   val no_facts: (indexname * term option) list
 end;
 
@@ -23,29 +23,29 @@
 val thisN = "this";
 val assmsN = "assms";
 
-fun strip_judgment thy = Object_Logic.drop_judgment thy o Logic.strip_assums_concl;
+fun strip_judgment ctxt = Object_Logic.drop_judgment ctxt o Logic.strip_assums_concl;
 
-fun statement_binds thy name prop =
-  [((name, 0), SOME (fold_rev Term.abs (Logic.strip_params prop) (strip_judgment thy prop)))];
+fun statement_binds ctxt name prop =
+  [((name, 0), SOME (fold_rev Term.abs (Logic.strip_params prop) (strip_judgment ctxt prop)))];
 
 
 (* goal *)
 
-fun goal thy [prop] = statement_binds thy thesisN prop
+fun goal ctxt [prop] = statement_binds ctxt thesisN prop
   | goal _ _ = [((thesisN, 0), NONE)];
 
 
 (* facts *)
 
-fun get_arg thy prop =
-  (case strip_judgment thy prop of
+fun get_arg ctxt prop =
+  (case strip_judgment ctxt prop of
     _ $ t => SOME (fold_rev Term.abs (Logic.strip_params prop) t)
   | _ => NONE);
 
 fun facts _ [] = []
-  | facts thy props =
+  | facts ctxt props =
       let val prop = List.last props
-      in [(Syntax_Ext.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end;
+      in [(Syntax_Ext.dddot_indexname, get_arg ctxt prop)] @ statement_binds ctxt thisN prop end;
 
 val no_facts = [(Syntax_Ext.dddot_indexname, NONE), ((thisN, 0), NONE)];
 
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Pure/Isar/element.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -197,13 +197,12 @@
 
 local
 
-fun standard_elim th =
-  (case Object_Logic.elim_concl th of
+fun standard_elim ctxt th =
+  (case Object_Logic.elim_concl ctxt th of
     SOME C =>
       let
-        val thy = Thm.theory_of_thm th;
         val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C);
-        val th' = Thm.instantiate ([], [(Thm.global_cterm_of thy C, Thm.global_cterm_of thy thesis)]) th;
+        val th' = Thm.instantiate ([], [apply2 (Thm.cterm_of ctxt) (C, thesis)]) th;
       in (th', true) end
   | NONE => (th, false));
 
@@ -227,13 +226,11 @@
 
 fun pretty_statement ctxt kind raw_th =
   let
-    val thy = Proof_Context.theory_of ctxt;
-
-    val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf ctxt raw_th);
+    val (th, is_elim) = standard_elim ctxt (Raw_Simplifier.norm_hhf ctxt raw_th);
     val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body true ctxt);
     val prop = Thm.prop_of th';
     val (prems, concl) = Logic.strip_horn prop;
-    val concl_term = Object_Logic.drop_judgment thy concl;
+    val concl_term = Object_Logic.drop_judgment ctxt concl;
 
     val fixes = fold_aterms (fn v as Free (x, T) =>
         if Variable.is_newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Pure/Isar/expression.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -622,16 +622,15 @@
 
 val introN = "intro";
 
-fun atomize_spec thy ts =
+fun atomize_spec ctxt ts =
   let
     val t = Logic.mk_conjunction_balanced ts;
-    val body = Object_Logic.atomize_term thy t;
+    val body = Object_Logic.atomize_term ctxt t;
     val bodyT = Term.fastype_of body;
   in
     if bodyT = propT
-    then (t, propT, Thm.reflexive (Thm.global_cterm_of thy t))
-    else
-      (body, bodyT, Object_Logic.atomize (Proof_Context.init_global thy) (Thm.global_cterm_of thy t))
+    then (t, propT, Thm.reflexive (Thm.cterm_of ctxt t))
+    else (body, bodyT, Object_Logic.atomize ctxt (Thm.cterm_of ctxt t))
   end;
 
 (* achieve plain syntax for locale predicates (without "PROP") *)
@@ -658,7 +657,9 @@
   let
     val name = Sign.full_name thy binding;
 
-    val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
+    val thy_ctxt = Proof_Context.init_global thy;
+
+    val (body, bodyT, body_eq) = atomize_spec thy_ctxt norm_ts;
     val env = Term.add_free_names body [];
     val xs = filter (member (op =) env o #1) parms;
     val Ts = map #2 xs;
@@ -669,7 +670,7 @@
 
     val args = map Logic.mk_type extraTs @ map Free xs;
     val head = Term.list_comb (Const (name, predT), args);
-    val statement = Object_Logic.ensure_propT thy head;
+    val statement = Object_Logic.ensure_propT thy_ctxt head;
 
     val ([pred_def], defs_thy) =
       thy
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Pure/Isar/object_logic.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -6,26 +6,26 @@
 
 signature OBJECT_LOGIC =
 sig
-  val get_base_sort: theory -> sort option
+  val get_base_sort: Proof.context -> sort option
   val add_base_sort: sort -> theory -> theory
   val add_judgment: binding * typ * mixfix -> theory -> theory
   val add_judgment_cmd: binding * string * mixfix -> theory -> theory
-  val judgment_name: theory -> string
-  val is_judgment: theory -> term -> bool
-  val drop_judgment: theory -> term -> term
-  val fixed_judgment: theory -> string -> term
-  val ensure_propT: theory -> term -> term
-  val dest_judgment: cterm -> cterm
-  val judgment_conv: conv -> conv
-  val elim_concl: thm -> term option
+  val judgment_name: Proof.context -> string
+  val is_judgment: Proof.context -> term -> bool
+  val drop_judgment: Proof.context -> term -> term
+  val fixed_judgment: Proof.context -> string -> term
+  val ensure_propT: Proof.context -> term -> term
+  val dest_judgment: Proof.context -> cterm -> cterm
+  val judgment_conv: Proof.context -> conv -> conv
+  val elim_concl: Proof.context -> thm -> term option
   val declare_atomize: attribute
   val declare_rulify: attribute
-  val atomize_term: theory -> term -> term
+  val atomize_term: Proof.context -> term -> term
   val atomize: Proof.context -> conv
   val atomize_prems: Proof.context -> conv
   val atomize_prems_tac: Proof.context -> int -> tactic
   val full_atomize_tac: Proof.context -> int -> tactic
-  val rulify_term: theory -> term -> term
+  val rulify_term: Proof.context -> term -> term
   val rulify_tac: Proof.context -> int -> tactic
   val rulify: Proof.context -> thm -> thm
   val rulify_no_asm: Proof.context -> thm -> thm
@@ -36,7 +36,7 @@
 structure Object_Logic: OBJECT_LOGIC =
 struct
 
-(** theory data **)
+(** context data **)
 
 datatype data = Data of
  {base_sort: sort option,
@@ -46,7 +46,7 @@
 fun make_data (base_sort, judgment, atomize_rulify) =
   Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify};
 
-structure Data = Theory_Data
+structure Data = Generic_Data
 (
   type T = data;
   val empty = make_data (NONE, NONE, ([], []));
@@ -66,7 +66,7 @@
 fun map_data f = Data.map (fn (Data {base_sort, judgment, atomize_rulify}) =>
   make_data (f (base_sort, judgment, atomize_rulify)));
 
-fun get_data thy = Data.get thy |> (fn Data args => args);
+fun get_data ctxt = Data.get (Context.Proof ctxt) |> (fn Data args => args);
 
 
 
@@ -76,9 +76,10 @@
 
 val get_base_sort = #base_sort o get_data;
 
-fun add_base_sort S = map_data (fn (base_sort, judgment, atomize_rulify) =>
-  if is_some base_sort then error "Attempt to redeclare object-logic base sort"
-  else (SOME S, judgment, atomize_rulify));
+fun add_base_sort S =
+  (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) =>
+    if is_some base_sort then error "Attempt to redeclare object-logic base sort"
+    else (SOME S, judgment, atomize_rulify));
 
 
 (* add judgment *)
@@ -90,7 +91,7 @@
     thy
     |> add_consts [(b, T, mx)]
     |> (fn thy' => Theory.add_deps_global c (c, Sign.the_const_type thy' c) [] thy')
-    |> map_data (fn (base_sort, judgment, atomize_rulify) =>
+    |> (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) =>
         if is_some judgment then error "Attempt to redeclare object-logic judgment"
         else (base_sort, SOME c, atomize_rulify))
   end;
@@ -105,51 +106,50 @@
 
 (* judgments *)
 
-fun judgment_name thy =
-  (case #judgment (get_data thy) of
+fun judgment_name ctxt =
+  (case #judgment (get_data ctxt) of
     SOME name => name
   | _ => raise TERM ("Unknown object-logic judgment", []));
 
-fun is_judgment thy (Const (c, _) $ _) = c = judgment_name thy
+fun is_judgment ctxt (Const (c, _) $ _) = c = judgment_name ctxt
   | is_judgment _ _ = false;
 
-fun drop_judgment thy (Abs (x, T, t)) = Abs (x, T, drop_judgment thy t)
-  | drop_judgment thy (tm as (Const (c, _) $ t)) =
-      if (c = judgment_name thy handle TERM _ => false) then t else tm
+fun drop_judgment ctxt (Abs (x, T, t)) = Abs (x, T, drop_judgment ctxt t)
+  | drop_judgment ctxt (tm as (Const (c, _) $ t)) =
+      if (c = judgment_name ctxt handle TERM _ => false) then t else tm
   | drop_judgment _ tm = tm;
 
-fun fixed_judgment thy x =
+fun fixed_judgment ctxt x =
   let  (*be robust wrt. low-level errors*)
-    val c = judgment_name thy;
+    val c = judgment_name ctxt;
     val aT = TFree (Name.aT, []);
     val T =
-      the_default (aT --> propT) (Sign.const_type thy c)
+      the_default (aT --> propT) (Sign.const_type (Proof_Context.theory_of ctxt) c)
       |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
     val U = Term.domain_type T handle Match => aT;
   in Const (c, T) $ Free (x, U) end;
 
-fun ensure_propT thy t =
+fun ensure_propT ctxt t =
   let val T = Term.fastype_of t
-  in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end;
+  in if T = propT then t else Const (judgment_name ctxt, T --> propT) $ t end;
 
-fun dest_judgment ct =
-  if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct)
+fun dest_judgment ctxt ct =
+  if is_judgment ctxt (Thm.term_of ct)
   then Thm.dest_arg ct
   else raise CTERM ("dest_judgment", [ct]);
 
-fun judgment_conv cv ct =
-  if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct)
+fun judgment_conv ctxt cv ct =
+  if is_judgment ctxt (Thm.term_of ct)
   then Conv.arg_conv cv ct
   else raise CTERM ("judgment_conv", [ct]);
 
 
 (* elimination rules *)
 
-fun elim_concl rule =
+fun elim_concl ctxt rule =
   let
-    val thy = Thm.theory_of_thm rule;
     val concl = Thm.concl_of rule;
-    val C = drop_judgment thy concl;
+    val C = drop_judgment ctxt concl;
   in
     if Term.is_Var C andalso
       exists (fn prem => concl aconv Logic.strip_assums_concl prem) (Thm.prems_of rule)
@@ -171,19 +171,19 @@
 fun add_rulify th = map_data (fn (base_sort, judgment, (atomize, rulify)) =>
   (base_sort, judgment, (atomize, Thm.add_thm th rulify)));
 
-val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
-val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
+val declare_atomize = Thm.declaration_attribute add_atomize;
+val declare_rulify = Thm.declaration_attribute add_rulify;
 
-val _ = Theory.setup (fold add_rulify Drule.norm_hhf_eqs);
+val _ = Theory.setup (fold (Context.theory_map o add_rulify) Drule.norm_hhf_eqs);
 
 
 (* atomize *)
 
-fun atomize_term thy =
-  drop_judgment thy o Raw_Simplifier.rewrite_term thy (get_atomize thy) [];
+fun atomize_term ctxt =
+  drop_judgment ctxt o
+    Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) (get_atomize ctxt) [];
 
-fun atomize ctxt =
-  Raw_Simplifier.rewrite ctxt true (get_atomize (Proof_Context.theory_of ctxt));
+fun atomize ctxt = Raw_Simplifier.rewrite ctxt true (get_atomize ctxt);
 
 fun atomize_prems ctxt ct =
   if Logic.has_meta_prems (Thm.term_of ct) then
@@ -196,11 +196,13 @@
 
 (* rulify *)
 
-fun rulify_term thy = Raw_Simplifier.rewrite_term thy (get_rulify thy) [];
-fun rulify_tac ctxt = rewrite_goal_tac ctxt (get_rulify (Proof_Context.theory_of ctxt));
+fun rulify_term ctxt =
+  Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) (get_rulify ctxt) [];
+
+fun rulify_tac ctxt = rewrite_goal_tac ctxt (get_rulify ctxt);
 
 fun gen_rulify full ctxt =
-  Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify (Proof_Context.theory_of ctxt)))
+  Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify ctxt))
   #> Drule.gen_all (Variable.maxidx_of ctxt)
   #> Thm.strip_shyps
   #> Drule.zero_var_indexes;
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -73,10 +73,8 @@
 
 fun eliminate fix_ctxt rule xs As thm =
   let
-    val thy = Proof_Context.theory_of fix_ctxt;
-
     val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm);
-    val _ = Object_Logic.is_judgment thy (Thm.concl_of thm) orelse
+    val _ = Object_Logic.is_judgment fix_ctxt (Thm.concl_of thm) orelse
       error "Conclusion in obtained context must be object-logic judgment";
 
     val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt;
@@ -99,9 +97,8 @@
 
 fun bind_judgment ctxt name =
   let
-    val thy = Proof_Context.theory_of ctxt;
     val ([x], ctxt') = Proof_Context.add_fixes [(Binding.name name, NONE, NoSyn)] ctxt;
-    val (t as _ $ Free v) = Object_Logic.fixed_judgment thy x;
+    val (t as _ $ Free v) = Object_Logic.fixed_judgment ctxt x;
   in ((v, t), ctxt') end;
 
 val thatN = "that";
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -406,9 +406,8 @@
 
 fun no_goal_cases st = map (rpair NONE) (goals st);
 
-fun goal_cases st =
-  Rule_Cases.make_common
-    (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
+fun goal_cases ctxt st =
+  Rule_Cases.make_common ctxt (Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
 
 fun apply_method text ctxt state =
   #2 (#2 (find_goal state)) |> (fn {statement, using, goal, before_qed, after_qed} =>
@@ -416,7 +415,7 @@
     |> Seq.map (fn (meth_cases, goal') =>
       state
       |> map_goal
-          (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #>
+          (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases ctxt goal') #>
            Proof_Context.update_cases true meth_cases)
           (K (statement, using, goal', before_qed, after_qed)) I));
 
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -842,7 +842,7 @@
 fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
   | drop_schematic b = b;
 
-fun auto_bind f ts ctxt = ctxt |> bind_terms (map drop_schematic (f (theory_of ctxt) ts));
+fun auto_bind f ts ctxt = ctxt |> bind_terms (map drop_schematic (f ctxt ts));
 
 val auto_bind_goal = auto_bind Auto_Bind.goal;
 val auto_bind_facts = auto_bind Auto_Bind.facts;
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -13,7 +13,7 @@
   type cases_tactic = thm -> cases_state Seq.seq
   val CASES: cases -> tactic -> cases_tactic
   val EMPTY_CASES: tactic -> cases_tactic
-  val SUBGOAL_CASES: ((term * int * thm) -> cases_tactic) -> int -> cases_tactic
+  val SUBGOAL_CASES: (term * int -> cases_tactic) -> int -> cases_tactic
   val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
 end
 
@@ -27,9 +27,9 @@
     cases: (string * T) list}
   val case_hypsN: string
   val strip_params: term -> (string * typ) list
-  val make_common: theory * term ->
+  val make_common: Proof.context -> term ->
     ((string * string list) * string list) list -> cases
-  val make_nested: term -> theory * term ->
+  val make_nested: Proof.context -> term -> term ->
     ((string * string list) * string list) list -> cases
   val apply: term list -> T -> T
   val consume: Proof.context -> thm list -> thm list -> ('a * int) * thm ->
@@ -107,9 +107,9 @@
 
 fun bindings args = map (apfst Binding.name) args;
 
-fun extract_case thy (case_outline, raw_prop) name hyp_names concls =
+fun extract_case ctxt (case_outline, raw_prop) name hyp_names concls =
   let
-    val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
+    val props = Logic.dest_conjunctions (Drule.norm_hhf (Proof_Context.theory_of ctxt) raw_prop);
     val len = length props;
     val nested = is_some case_outline andalso len > 1;
 
@@ -126,7 +126,7 @@
           extract_assumes name hyp_names case_outline prop
           |> apply2 (map (apsnd (maps Logic.dest_conjunctions)));
 
-        val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
+        val concl = Object_Logic.drop_judgment ctxt (Logic.strip_assums_concl prop);
         val binds =
           (case_conclN, concl) :: dest_binops concls concl
           |> map (fn (x, t) => ((x, 0), SOME (abs_fixes t)));
@@ -152,7 +152,7 @@
     else SOME (nested_case (hd cases))
   end;
 
-fun make rule_struct (thy, prop) cases =
+fun make ctxt rule_struct prop cases =
   let
     val n = length cases;
     val nprems = Logic.count_prems prop;
@@ -160,13 +160,13 @@
       ((case try (fn () =>
           (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
         NONE => (name, NONE)
-      | SOME p => (name, extract_case thy p name hyp_names concls)) :: cs, i - 1);
+      | SOME p => (name, extract_case ctxt p name hyp_names concls)) :: cs, i - 1);
   in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end;
 
 in
 
-val make_common = make NONE;
-fun make_nested rule_struct = make (SOME rule_struct);
+fun make_common ctxt = make ctxt NONE;
+fun make_nested ctxt rule_struct = make ctxt (SOME rule_struct);
 
 fun apply args =
   let
@@ -192,7 +192,7 @@
 
 fun SUBGOAL_CASES tac i st =
   (case try Logic.nth_prem (i, Thm.prop_of st) of
-    SOME goal => tac (goal, i, st) st
+    SOME goal => tac (goal, i) st
   | NONE => Seq.empty);
 
 fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Pure/Isar/specification.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -356,7 +356,7 @@
         val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
         val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
 
-        val thesis = Object_Logic.fixed_judgment (Proof_Context.theory_of ctxt) Auto_Bind.thesisN;
+        val thesis = Object_Logic.fixed_judgment ctxt Auto_Bind.thesisN;
 
         fun assume_case ((name, (vars, _)), asms) ctxt' =
           let
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Pure/Isar/typedecl.ML
--- a/src/Pure/Isar/typedecl.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Pure/Isar/typedecl.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -26,11 +26,6 @@
 
 (* primitives *)
 
-fun object_logic_arity name thy =
-  (case Object_Logic.get_base_sort thy of
-    NONE => thy
-  | SOME S => Axclass.arity_axiomatization (name, replicate (Sign.arity_number thy name) S, S) thy);
-
 fun basic_decl decl (b, n, mx) lthy =
   let val name = Local_Theory.full_name lthy b in
     lthy
@@ -41,8 +36,11 @@
   end;
 
 fun basic_typedecl (b, n, mx) lthy =
-  basic_decl (fn name => Sign.add_type lthy (b, n, NoSyn) #> object_logic_arity name)
-    (b, n, mx) lthy;
+  basic_decl (fn name =>
+    Sign.add_type lthy (b, n, NoSyn) #>
+    (case Object_Logic.get_base_sort lthy of
+      SOME S => Axclass.arity_axiomatization (name, replicate n S, S)
+    | NONE => I)) (b, n, mx) lthy;
 
 
 (* global type -- without dependencies on type parameters of the context *)
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Pure/Thy/term_style.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -49,8 +49,7 @@
 
 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
   let
-    val concl =
-      Object_Logic.drop_judgment (Proof_Context.theory_of ctxt) (Logic.strip_imp_concl t)
+    val concl = Object_Logic.drop_judgment ctxt (Logic.strip_imp_concl t);
   in
     (case concl of
       _ $ l $ r => proj (l, r)
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -89,7 +89,7 @@
 
 (* matching theorems *)
 
-fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
+fun is_nontrivial ctxt = Term.is_Const o Term.head_of o Object_Logic.drop_judgment ctxt;
 
 (*extract terms from term_src, refine them to the parts that concern us,
   if po try match them against obj else vice versa.
@@ -100,7 +100,7 @@
     val thy = Proof_Context.theory_of ctxt;
 
     fun matches pat =
-      is_nontrivial thy pat andalso
+      is_nontrivial ctxt pat andalso
       Pattern.matches thy (if po then (pat, obj) else (obj, pat));
 
     fun subst_size pat =
@@ -171,8 +171,7 @@
     in
       (*elim rules always have assumptions, so an elim with one
         assumption is as good as an intro rule with none*)
-      if is_nontrivial (Proof_Context.theory_of ctxt) (Thm.major_prem_of thm)
-          andalso not (null successful) then
+      if is_nontrivial ctxt (Thm.major_prem_of thm) andalso not (null successful) then
         SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm - 1, foldl1 Int.min successful)
       else NONE
     end
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Pure/more_thm.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -68,6 +68,8 @@
   val forall_intr_frees: thm -> thm
   val unvarify_global: thm -> thm
   val close_derivation: thm -> thm
+  val rename_params_rule: string list * int -> thm -> thm
+  val rename_boundvars: term -> term -> thm -> thm
   val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory
   val add_axiom_global: binding * term -> theory -> (string * thm) * theory
   val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory
@@ -392,6 +394,38 @@
   else thm;
 
 
+(* user renaming of parameters in a subgoal *)
+
+(*The names, if distinct, are used for the innermost parameters of subgoal i;
+  preceding parameters may be renamed to make all parameters distinct.*)
+fun rename_params_rule (names, i) st =
+  let
+    val (_, Bs, Bi, C) = Thm.dest_state (st, i);
+    val params = map #1 (Logic.strip_params Bi);
+    val short = length params - length names;
+    val names' =
+      if short < 0 then error "More names than parameters in subgoal!"
+      else Name.variant_list names (take short params) @ names;
+    val free_names = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
+    val Bi' = Logic.list_rename_params names' Bi;
+  in
+    (case duplicates (op =) names of
+      a :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ a); st)
+    | [] =>
+      (case inter (op =) names free_names of
+        a :: _ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); st)
+      | [] => Thm.renamed_prop (Logic.list_implies (Bs @ [Bi'], C)) st))
+  end;
+
+
+(* preservation of bound variable names *)
+
+fun rename_boundvars pat obj th =
+  (case Term.rename_abs pat obj (Thm.prop_of th) of
+    NONE => th
+  | SOME prop' => Thm.renamed_prop prop' th);
+
+
 
 (** specification primitives **)
 
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Pure/thm.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -34,6 +34,7 @@
   val maxidx_of_cterm: cterm -> int
   val global_cterm_of: theory -> term -> cterm
   val cterm_of: Proof.context -> term -> cterm
+  val renamed_term: term -> cterm -> cterm
   val dest_comb: cterm -> cterm * cterm
   val dest_fun: cterm -> cterm
   val dest_arg: cterm -> cterm
@@ -81,6 +82,7 @@
   val cprop_of: thm -> cterm
   val cprem_of: thm -> int -> cterm
   val transfer: theory -> thm -> thm
+  val renamed_prop: term -> thm -> thm
   val weaken: cterm -> thm -> thm
   val weaken_sorts: sort list -> cterm -> cterm
   val extra_shyps: thm -> sort list
@@ -125,14 +127,13 @@
   val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
   val varifyT_global: thm -> thm
   val legacy_freezeT: thm -> thm
+  val dest_state: thm * int -> (term * term) list * term list * term * term
   val lift_rule: cterm -> thm -> thm
   val incr_indexes: int -> thm -> thm
   val assumption: Proof.context option -> int -> thm -> thm Seq.seq
   val eq_assumption: int -> thm -> thm
   val rotate_rule: int -> int -> thm -> thm
   val permute_prems: int -> int -> thm -> thm
-  val rename_params_rule: string list * int -> thm -> thm
-  val rename_boundvars: term -> term -> thm -> thm
   val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} ->
     bool * thm * int -> int -> thm -> thm Seq.seq
   val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
@@ -195,6 +196,10 @@
 
 val cterm_of = global_cterm_of o Proof_Context.theory_of;
 
+fun renamed_term t' (Cterm {thy, t, T, maxidx, sorts}) =
+  if t aconv t' then Cterm {thy = thy, t = t', T = T, maxidx = maxidx, sorts = sorts}
+  else raise TERM ("renamed_term: terms disagree", [t, t']);
+
 fun merge_thys0 (Cterm {thy = thy1, ...}) (Cterm {thy = thy2, ...}) =
   Theory.merge (thy1, thy2);
 
@@ -416,6 +421,13 @@
         prop = prop})
   end;
 
+(*implicit alpha-conversion*)
+fun renamed_prop prop' (Thm (der, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) =
+  if prop aconv prop' then
+    Thm (der, {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps,
+      hyps = hyps, tpairs = tpairs, prop = prop'})
+  else raise TERM ("renamed_prop: props disagree", [prop, prop']);
+
 fun make_context NONE thy = Context.Theory thy
   | make_context (SOME ctxt) thy =
       if Theory.subthy (thy, Proof_Context.theory_of ctxt) then Context.Proof ctxt
@@ -1426,56 +1438,6 @@
   end;
 
 
-(** User renaming of parameters in a subgoal **)
-
-(*Calls error rather than raising an exception because it is intended
-  for top-level use -- exception handling would not make sense here.
-  The names in cs, if distinct, are used for the innermost parameters;
-  preceding parameters may be renamed to make all params distinct.*)
-fun rename_params_rule (cs, i) state =
-  let
-    val Thm (der, {thy, tags, maxidx, shyps, hyps, ...}) = state;
-    val (tpairs, Bs, Bi, C) = dest_state (state, i);
-    val iparams = map #1 (Logic.strip_params Bi);
-    val short = length iparams - length cs;
-    val newnames =
-      if short < 0 then error "More names than abstractions!"
-      else Name.variant_list cs (take short iparams) @ cs;
-    val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
-    val newBi = Logic.list_rename_params newnames Bi;
-  in
-    (case duplicates (op =) cs of
-      a :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ a); state)
-    | [] =>
-      (case inter (op =) cs freenames of
-        a :: _ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); state)
-      | [] =>
-        Thm (der,
-         {thy = thy,
-          tags = tags,
-          maxidx = maxidx,
-          shyps = shyps,
-          hyps = hyps,
-          tpairs = tpairs,
-          prop = Logic.list_implies (Bs @ [newBi], C)})))
-  end;
-
-
-(*** Preservation of bound variable names ***)
-
-fun rename_boundvars pat obj (thm as Thm (der, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) =
-  (case Term.rename_abs pat obj prop of
-    NONE => thm
-  | SOME prop' => Thm (der,
-      {thy = thy,
-       tags = tags,
-       maxidx = maxidx,
-       hyps = hyps,
-       shyps = shyps,
-       tpairs = tpairs,
-       prop = prop'}));
-
-
 (* strip_apply f B A strips off all assumptions/parameters from A
    introduced by lifting over B, and applies f to remaining part of A*)
 fun strip_apply f =
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Tools/atomize_elim.ML
--- a/src/Tools/atomize_elim.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Tools/atomize_elim.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -55,7 +55,7 @@
 fun atomize_elim_conv ctxt ct =
     (forall_conv (prems_conv ~1 o Object_Logic.atomize_prems o snd) ctxt
     then_conv Raw_Simplifier.rewrite ctxt true (Named_Theorems.get ctxt named_theorems)
-    then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
+    then_conv (fn ct' => if can (Object_Logic.dest_judgment ctxt) ct'
                          then all_conv ct'
                          else raise CTERM ("atomize_elim", [ct', ct])))
     ct
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Tools/induct.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -59,11 +59,11 @@
   val arbitrary_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
   val add_defs: (binding option * (term * bool)) option list -> Proof.context ->
     (term option list * thm list) * Proof.context
-  val atomize_term: theory -> term -> term
+  val atomize_term: Proof.context -> term -> term
   val atomize_cterm: Proof.context -> conv
   val atomize_tac: Proof.context -> int -> tactic
   val inner_atomize_tac: Proof.context -> int -> tactic
-  val rulified_term: thm -> theory * term
+  val rulified_term: Proof.context -> thm -> term
   val rulify_tac: Proof.context -> int -> tactic
   val simplified_rule: Proof.context -> thm -> thm
   val simplify_tac: Proof.context -> int -> tactic
@@ -75,7 +75,7 @@
     thm list -> int -> cases_tactic
   val get_inductT: Proof.context -> term option list list -> thm list list
   type case_data = (((string * string list) * string list) list * int) (* FIXME -> rule_cases.ML *)
-  val gen_induct_tac: (theory -> case_data * thm -> case_data * thm) ->
+  val gen_induct_tac: (case_data * thm -> case_data * thm) ->
     Proof.context -> bool -> (binding option * (term * bool)) option list list ->
     (string * typ) list list -> term option list -> thm list option ->
     thm list -> int -> cases_tactic
@@ -137,14 +137,12 @@
       Conv.implies_concl_conv (swap_prems_conv (i - 1)) then_conv
       Conv.rewr_conv Drule.swap_prems_eq
 
-fun drop_judgment ctxt = Object_Logic.drop_judgment (Proof_Context.theory_of ctxt);
-
 fun find_eq ctxt t =
   let
     val l = length (Logic.strip_params t);
     val Hs = Logic.strip_assums_hyp t;
     fun find (i, t) =
-      (case Induct_Args.dest_def (drop_judgment ctxt t) of
+      (case Induct_Args.dest_def (Object_Logic.drop_judgment ctxt t) of
         SOME (Bound j, _) => SOME (i, j)
       | SOME (_, Bound j) => SOME (i, j)
       | _ => NONE);
@@ -167,11 +165,11 @@
 
 (* rotate k premises to the left by j, skipping over first j premises *)
 
-fun rotate_conv 0 j 0 = Conv.all_conv
+fun rotate_conv 0 _ 0 = Conv.all_conv
   | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k - 1)
   | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i - 1) j k);
 
-fun rotate_tac j 0 = K all_tac
+fun rotate_tac _ 0 = K all_tac
   | rotate_tac j k = SUBGOAL (fn (goal, i) =>
       CONVERSION (rotate_conv
         j (length (Logic.strip_assums_hyp goal) - j - k) k) i);
@@ -181,7 +179,7 @@
 
 fun rulify_defs_conv ctxt ct =
   if exists_subterm (is_some o Induct_Args.dest_def) (Thm.term_of ct) andalso
-    not (is_some (Induct_Args.dest_def (drop_judgment ctxt (Thm.term_of ct))))
+    not (is_some (Induct_Args.dest_def (Object_Logic.drop_judgment ctxt (Thm.term_of ct))))
   then
     (Conv.forall_conv (rulify_defs_conv o snd) ctxt else_conv
      Conv.implies_conv (Conv.try_conv (rulify_defs_conv ctxt))
@@ -502,8 +500,8 @@
           val rule' = rule
             |> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt);
         in
-          CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt,
-              Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
+          CASES (Rule_Cases.make_common ctxt
+              (Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
             ((Method.insert_tac more_facts THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
                 (if simp then TRY o trivial_tac ctxt else K all_tac)) i) st
         end)
@@ -520,9 +518,9 @@
 
 (* atomize *)
 
-fun atomize_term thy =
-  Raw_Simplifier.rewrite_term thy Induct_Args.atomize []
-  #> Object_Logic.drop_judgment thy;
+fun atomize_term ctxt =
+  Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) Induct_Args.atomize []
+  #> Object_Logic.drop_judgment ctxt;
 
 fun atomize_cterm ctxt = Raw_Simplifier.rewrite ctxt true Induct_Args.atomize;
 
@@ -538,12 +536,11 @@
   Raw_Simplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #>
   Raw_Simplifier.rewrite_term thy Induct_Args.rulify_fallback [];
 
-fun rulified_term thm =
+fun rulified_term ctxt thm =
   let
-    val thy = Thm.theory_of_thm thm;
-    val rulify = rulify_term thy;
+    val rulify = rulify_term (Proof_Context.theory_of ctxt);
     val (As, B) = Logic.strip_horn (Thm.prop_of thm);
-  in (thy, Logic.list_implies (map rulify As, rulify B)) end;
+  in Logic.list_implies (map rulify As, rulify B) end;
 
 fun rulify_tac ctxt =
   rewrite_goal_tac ctxt (Induct_Args.rulify @ conjunction_congs) THEN'
@@ -606,7 +603,7 @@
 fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] =
       let
         val x = Name.clean (Variable.revert_fixed ctxt z);
-        fun index i [] = []
+        fun index _ [] = []
           | index i (y :: ys) =
               if x = y then x ^ string_of_int i :: index (i + 1) ys
               else y :: index i ys;
@@ -734,10 +731,8 @@
 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 =
-  SUBGOAL_CASES (fn (_, i, st) =>
+  SUBGOAL_CASES (fn (_, i) =>
     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;
 
@@ -745,9 +740,9 @@
         (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))
+          |> maps (prep_inst ctxt align_right (atomize_term ctxt))
           |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
-        |> mod_cases thy
+        |> mod_cases
         |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
 
       val ruleq =
@@ -766,7 +761,7 @@
           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 Rule_Cases.make_nested ctxt (Thm.prop_of rule'') (rulified_term ctxt rule'') cases' end;
     in
       fn st =>
         ruleq
@@ -800,7 +795,7 @@
         ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac ctxt) else K all_tac)
          THEN_ALL_NEW rulify_tac ctxt);
 
-val induct_tac = gen_induct_tac (K I);
+val induct_tac = gen_induct_tac I;
 
 
 
@@ -825,30 +820,27 @@
 
 in
 
-fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i, st) =>
+fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i) =>
   let
     fun inst_rule r =
       if null inst then `Rule_Cases.get r
       else Drule.cterm_instantiate (prep_inst ctxt align_right I (main_prop_of r, inst)) r
         |> pair (Rule_Cases.get r);
-
-    fun ruleq goal =
+  in
+    fn st =>
       (case opt_rule of
         SOME r => Seq.single (inst_rule r)
       | NONE =>
           (get_coinductP ctxt goal @ get_coinductT ctxt inst)
           |> tap (trace_rules ctxt coinductN)
-          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
-  in
-    fn st =>
-      ruleq goal
+          |> Seq.of_list |> Seq.maps (Seq.try inst_rule))
       |> Seq.maps (Rule_Cases.consume ctxt [] facts)
       |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
         guess_instance ctxt rule i st
         |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
         |> Seq.maps (fn rule' =>
-          CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt,
-              Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
+          CASES (Rule_Cases.make_common ctxt
+              (Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
             (Method.insert_tac more_facts i THEN resolve_tac ctxt [rule'] i) st))
   end);
 
diff -r 2fcf41a626f7 -r 8a53364a3143 src/Tools/induction.ML
--- a/src/Tools/induction.ML	Wed Apr 08 19:24:32 2015 +0200
+++ b/src/Tools/induction.ML	Wed Apr 08 22:15:03 2015 +0200
@@ -43,7 +43,7 @@
           (take n cases ~~ take n hnamess);
     in ((cases', consumes), th) end;
 
-val induction_tac = Induct.gen_induct_tac (K name_hyps);
+val induction_tac = Induct.gen_induct_tac name_hyps;
 
 val _ = Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_tac);