merged
authorwenzelm
Wed Apr 08 22:15:03 2015 +0200 (2015-04-08)
changeset 599798a53364a3143
parent 59967 2fcf41a626f7
parent 59978 c2dc7856e2e5
child 59980 070f04c94b2e
merged
     1.1 --- a/etc/symbols	Wed Apr 08 19:24:32 2015 +0200
     1.2 +++ b/etc/symbols	Wed Apr 08 22:15:03 2015 +0200
     1.3 @@ -347,6 +347,7 @@
     1.4  \<cedilla>              code: 0x0000b8
     1.5  \<hungarumlaut>         code: 0x0002dd
     1.6  \<some>                 code: 0x0003f5
     1.7 +\<hole>                 code: 0x002311
     1.8  \<newline>              code: 0x0023ce
     1.9  \<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
    1.10  \<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
    1.11 @@ -358,4 +359,3 @@
    1.12  \<^esub>                code: 0x0021d9  group: control_block  font: IsabelleText  abbrev: =_)
    1.13  \<^bsup>                code: 0x0021d7  group: control_block  font: IsabelleText  abbrev: =^(
    1.14  \<^esup>                code: 0x0021d6  group: control_block  font: IsabelleText  abbrev: =^)
    1.15 -
     2.1 --- a/lib/fonts/IsabelleText.sfd	Wed Apr 08 19:24:32 2015 +0200
     2.2 +++ b/lib/fonts/IsabelleText.sfd	Wed Apr 08 22:15:03 2015 +0200
     2.3 @@ -19,7 +19,7 @@
     2.4  OS2_WeightWidthSlopeOnly: 0
     2.5  OS2_UseTypoMetrics: 1
     2.6  CreationTime: 1050361371
     2.7 -ModificationTime: 1392668982
     2.8 +ModificationTime: 1428519538
     2.9  PfmFamily: 17
    2.10  TTFWeight: 400
    2.11  TTFWidth: 5
    2.12 @@ -2242,7 +2242,7 @@
    2.13  FitToEm: 1
    2.14  WinInfo: 8912 16 10
    2.15  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
    2.16 -BeginChars: 1114189 1096
    2.17 +BeginChars: 1114189 1097
    2.18  
    2.19  StartChar: u10000
    2.20  Encoding: 65536 65536 0
    2.21 @@ -55594,5 +55594,25 @@
    2.22   268.5 122 l 17,5,-1
    2.23  EndSplineSet
    2.24  EndChar
    2.25 +
    2.26 +StartChar: uni2311
    2.27 +Encoding: 8977 8977 1096
    2.28 +Width: 1233
    2.29 +Flags: W
    2.30 +LayerCount: 2
    2.31 +Fore
    2.32 +SplineSet
    2.33 +231 394 m 1,0,1
    2.34 + 616 531 616 531 1001 394 c 1,2,3
    2.35 + 864 778 864 778 1001 1164 c 1,4,5
    2.36 + 616 1026 616 1026 231 1164 c 1,6,7
    2.37 + 368 778 368 778 231 394 c 1,0,1
    2.38 +97 258 m 1,8,9
    2.39 + 281 758 281 758 97 1298 c 1,10,11
    2.40 + 616 1121 616 1121 1136 1298 c 1,12,13
    2.41 + 952 798 952 798 1136 259 c 1,14,15
    2.42 + 616 436 616 436 97 258 c 1,8,9
    2.43 +EndSplineSet
    2.44 +EndChar
    2.45  EndChars
    2.46  EndSplineFont
     3.1 Binary file lib/fonts/IsabelleText.ttf has changed
     4.1 --- a/lib/fonts/IsabelleTextBold.sfd	Wed Apr 08 19:24:32 2015 +0200
     4.2 +++ b/lib/fonts/IsabelleTextBold.sfd	Wed Apr 08 22:15:03 2015 +0200
     4.3 @@ -19,7 +19,7 @@
     4.4  OS2_WeightWidthSlopeOnly: 0
     4.5  OS2_UseTypoMetrics: 1
     4.6  CreationTime: 1050374980
     4.7 -ModificationTime: 1392669044
     4.8 +ModificationTime: 1428519645
     4.9  PfmFamily: 17
    4.10  TTFWeight: 700
    4.11  TTFWidth: 5
    4.12 @@ -1675,7 +1675,7 @@
    4.13  AntiAlias: 1
    4.14  FitToEm: 1
    4.15  WinInfo: 8928 16 10
    4.16 -BeginChars: 1114112 1085
    4.17 +BeginChars: 1114112 1086
    4.18  
    4.19  StartChar: u10000
    4.20  Encoding: 65536 65536 0
    4.21 @@ -58524,5 +58524,25 @@
    4.22   298 187 l 17,5,-1
    4.23  EndSplineSet
    4.24  EndChar
    4.25 +
    4.26 +StartChar: uni2311
    4.27 +Encoding: 8977 8977 1085
    4.28 +Width: 1233
    4.29 +Flags: W
    4.30 +LayerCount: 2
    4.31 +Fore
    4.32 +SplineSet
    4.33 +250 412 m 1,0,1
    4.34 + 616 544 616 544 982 412 c 1,2,3
    4.35 + 851 778 851 778 982 1144 c 1,4,5
    4.36 + 616 1014 616 1014 250 1144 c 1,6,7
    4.37 + 381 778 381 778 250 412 c 1,0,1
    4.38 +71 232 m 1,8,9
    4.39 + 264 756 264 756 71 1324 c 1,10,11
    4.40 + 616 1138 616 1138 1162 1324 c 1,12,13
    4.41 + 969 800 969 800 1162 234 c 1,14,15
    4.42 + 617 418 617 418 71 232 c 1,8,9
    4.43 +EndSplineSet
    4.44 +EndChar
    4.45  EndChars
    4.46  EndSplineFont
     5.1 Binary file lib/fonts/IsabelleTextBold.ttf has changed
     6.1 --- a/lib/texinputs/isabellesym.sty	Wed Apr 08 19:24:32 2015 +0200
     6.2 +++ b/lib/texinputs/isabellesym.sty	Wed Apr 08 22:15:03 2015 +0200
     6.3 @@ -356,5 +356,5 @@
     6.4  \newcommand{\isasymsome}{\isamath{\epsilon\,}}
     6.5  \newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}
     6.6  \newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
     6.7 +\newcommand{\isasymhole}{\isatext{\rm\wasylozenge}}  %requires wasysym
     6.8  \newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
     6.9 -
     7.1 --- a/src/Doc/Isar_Ref/document/root.tex	Wed Apr 08 19:24:32 2015 +0200
     7.2 +++ b/src/Doc/Isar_Ref/document/root.tex	Wed Apr 08 22:15:03 2015 +0200
     7.3 @@ -1,6 +1,7 @@
     7.4  \documentclass[12pt,a4paper,fleqn]{report}
     7.5  \usepackage[T1]{fontenc}
     7.6  \usepackage{amssymb}
     7.7 +\usepackage{wasysym}
     7.8  \usepackage{eurosym}
     7.9  \usepackage[english]{babel}
    7.10  \usepackage[only,bigsqcap]{stmaryrd}
     8.1 --- a/src/FOL/simpdata.ML	Wed Apr 08 19:24:32 2015 +0200
     8.2 +++ b/src/FOL/simpdata.ML	Wed Apr 08 22:15:03 2015 +0200
     8.3 @@ -88,7 +88,7 @@
     8.4  
     8.5  structure Splitter = Splitter
     8.6  (
     8.7 -  val thy = @{theory}
     8.8 +  val context = @{context}
     8.9    val mk_eq = mk_eq
    8.10    val meta_eq_to_iff = @{thm meta_eq_to_iff}
    8.11    val iffD = @{thm iffD2}
     9.1 --- a/src/HOL/Decision_Procs/approximation.ML	Wed Apr 08 19:24:32 2015 +0200
     9.2 +++ b/src/HOL/Decision_Procs/approximation.ML	Wed Apr 08 22:15:03 2015 +0200
     9.3 @@ -50,7 +50,7 @@
     9.4  
     9.5  (* Should be in HOL.thy ? *)
     9.6  fun gen_eval_tac conv ctxt = CONVERSION
     9.7 -  (Object_Logic.judgment_conv (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt))
     9.8 +  (Object_Logic.judgment_conv ctxt (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt))
     9.9    THEN' rtac TrueI
    9.10  
    9.11  val form_equations = @{thms interpret_form_equations};
    10.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Wed Apr 08 19:24:32 2015 +0200
    10.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Wed Apr 08 22:15:03 2015 +0200
    10.3 @@ -226,7 +226,7 @@
    10.4    | SOME instance =>
    10.5        Object_Logic.full_atomize_tac ctxt i THEN
    10.6        simp_tac (put_simpset (#simpset (snd instance)) ctxt) i THEN  (* FIXME already part of raw_ferrack_qe_conv? *)
    10.7 -      CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
    10.8 +      CONVERSION (Object_Logic.judgment_conv ctxt (raw_ferrack_qe_conv ctxt instance)) i THEN
    10.9        simp_tac ctxt i));  (* FIXME really? *)
   10.10  
   10.11  end;
    11.1 --- a/src/HOL/Decision_Procs/langford.ML	Wed Apr 08 19:24:32 2015 +0200
    11.2 +++ b/src/HOL/Decision_Procs/langford.ML	Wed Apr 08 22:15:03 2015 +0200
    11.3 @@ -261,6 +261,6 @@
    11.4        THEN (CONVERSION Thm.eta_long_conversion) i
    11.5        THEN (TRY o generalize_tac (cfrees (#atoms instance))) i
    11.6        THEN Object_Logic.full_atomize_tac ctxt i
    11.7 -      THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ctxt ss instance)) i
    11.8 +      THEN CONVERSION (Object_Logic.judgment_conv ctxt (raw_dlo_conv ctxt ss instance)) i
    11.9        THEN (simp_tac (put_simpset ss ctxt) i)));
   11.10  end;
   11.11 \ No newline at end of file
    12.1 --- a/src/HOL/GCD.thy	Wed Apr 08 19:24:32 2015 +0200
    12.2 +++ b/src/HOL/GCD.thy	Wed Apr 08 22:15:03 2015 +0200
    12.3 @@ -49,8 +49,8 @@
    12.4  
    12.5  class semiring_gcd = comm_semiring_1 + gcd +
    12.6    assumes gcd_dvd1 [iff]: "gcd a b dvd a"
    12.7 -		and gcd_dvd2 [iff]: "gcd a b dvd b"
    12.8 -		and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b"
    12.9 +    and gcd_dvd2 [iff]: "gcd a b dvd b"
   12.10 +    and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b"
   12.11  
   12.12  class ring_gcd = comm_ring_1 + semiring_gcd
   12.13  
    13.1 --- a/src/HOL/HOL.thy	Wed Apr 08 19:24:32 2015 +0200
    13.2 +++ b/src/HOL/HOL.thy	Wed Apr 08 22:15:03 2015 +0200
    13.3 @@ -848,7 +848,7 @@
    13.4  apply (rule prem)
    13.5  apply assumption
    13.6  apply (rule allI)+
    13.7 -apply (tactic {* eresolve_tac @{context} [Classical.dup_elim NONE @{thm allE}] 1 *})
    13.8 +apply (tactic {* eresolve_tac @{context} [Classical.dup_elim @{context} @{thm allE}] 1 *})
    13.9  apply iprover
   13.10  done
   13.11  
    14.1 --- a/src/HOL/Library/Rewrite.thy	Wed Apr 08 19:24:32 2015 +0200
    14.2 +++ b/src/HOL/Library/Rewrite.thy	Wed Apr 08 22:15:03 2015 +0200
    14.3 @@ -1,17 +1,22 @@
    14.4 +(*  Title:      HOL/Library/Rewrite.thy
    14.5 +    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
    14.6 +
    14.7 +Proof method "rewrite" with support for subterm-selection based on patterns.
    14.8 +*)
    14.9 +
   14.10  theory Rewrite
   14.11  imports Main
   14.12  begin
   14.13  
   14.14 -consts rewrite_HOLE :: "'a :: {}"
   14.15 +consts rewrite_HOLE :: "'a::{}"
   14.16  notation rewrite_HOLE ("HOLE")
   14.17  notation rewrite_HOLE ("\<box>")
   14.18  
   14.19  lemma eta_expand:
   14.20 -  fixes f :: "'a :: {} \<Rightarrow> 'b :: {}" shows "f \<equiv> (\<lambda>x. f x)"
   14.21 -  by (rule reflexive)
   14.22 +  fixes f :: "'a::{} \<Rightarrow> 'b::{}"
   14.23 +  shows "f \<equiv> \<lambda>x. f x" .
   14.24  
   14.25  ML_file "cconv.ML"
   14.26  ML_file "rewrite.ML"
   14.27 -setup Rewrite.setup
   14.28  
   14.29  end
    15.1 --- a/src/HOL/Library/bnf_lfp_countable.ML	Wed Apr 08 19:24:32 2015 +0200
    15.2 +++ b/src/HOL/Library/bnf_lfp_countable.ML	Wed Apr 08 22:15:03 2015 +0200
    15.3 @@ -172,7 +172,7 @@
    15.4        Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
    15.5          mk_encode_injectives_tac ctxt ns induct nchotomys injectss rec_thmss map_comps'
    15.6            inj_map_strongs')
    15.7 -      |> HOLogic.conj_elims
    15.8 +      |> HOLogic.conj_elims ctxt
    15.9        |> Proof_Context.export names_ctxt ctxt
   15.10        |> map Thm.close_derivation
   15.11      end;
    16.1 --- a/src/HOL/Library/cconv.ML	Wed Apr 08 19:24:32 2015 +0200
    16.2 +++ b/src/HOL/Library/cconv.ML	Wed Apr 08 22:15:03 2015 +0200
    16.3 @@ -1,3 +1,9 @@
    16.4 +(*  Title:      HOL/Library/cconv.ML
    16.5 +    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
    16.6 +
    16.7 +FIXME!?
    16.8 +*)
    16.9 +
   16.10  infix 1 then_cconv
   16.11  infix 0 else_cconv
   16.12  
   16.13 @@ -170,7 +176,8 @@
   16.14  fun prems_cconv 0 cv ct = cv ct
   16.15    | prems_cconv n cv ct =
   16.16        (case ct |> Thm.term_of of
   16.17 -        (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
   16.18 +        (Const (@{const_name "Pure.imp"}, _) $ _) $ _ =>
   16.19 +          ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
   16.20        | _ =>  cv ct)
   16.21  
   16.22  (*rewrite B in A1 Pure.imp ... Pure.imp An Pure.imp B*)
   16.23 @@ -212,7 +219,7 @@
   16.24        end
   16.25    | NONE => raise THM ("gconv_rule", i, [th]))
   16.26  
   16.27 -  (* Conditional conversions as tactics. *)
   16.28 +(* Conditional conversions as tactics. *)
   16.29  fun CCONVERSION cv i st = Seq.single (gconv_rule cv i st)
   16.30    handle THM _ => Seq.empty
   16.31         | CTERM _ => Seq.empty
    17.1 --- a/src/HOL/Library/rewrite.ML	Wed Apr 08 19:24:32 2015 +0200
    17.2 +++ b/src/HOL/Library/rewrite.ML	Wed Apr 08 22:15:03 2015 +0200
    17.3 @@ -1,24 +1,26 @@
    17.4 -(* Author: Christoph Traut, Lars Noschinski
    17.5 +(*  Title:      HOL/Library/rewrite.ML
    17.6 +    Author:     Christoph Traut, Lars Noschinski, TU Muenchen
    17.7  
    17.8 -  This is a rewrite method supports subterm-selection based on patterns.
    17.9 +This is a rewrite method that supports subterm-selection based on patterns.
   17.10  
   17.11 -  The patterns accepted by rewrite are of the following form:
   17.12 -    <atom>    ::= <term> | "concl" | "asm" | "for" "(" <names> ")"
   17.13 -    <pattern> ::= (in <atom> | at <atom>) [<pattern>]
   17.14 -    <args>    ::= [<pattern>] ("to" <term>) <thms>
   17.15 +The patterns accepted by rewrite are of the following form:
   17.16 +  <atom>    ::= <term> | "concl" | "asm" | "for" "(" <names> ")"
   17.17 +  <pattern> ::= (in <atom> | at <atom>) [<pattern>]
   17.18 +  <args>    ::= [<pattern>] ("to" <term>) <thms>
   17.19  
   17.20 -  This syntax was clearly inspired by Gonthier's and Tassi's language of
   17.21 -  patterns but has diverged significantly during its development.
   17.22 +This syntax was clearly inspired by Gonthier's and Tassi's language of
   17.23 +patterns but has diverged significantly during its development.
   17.24  
   17.25 -  We also allow introduction of identifiers for bound variables,
   17.26 -  which can then be used to match arbitary subterms inside abstractions.
   17.27 +We also allow introduction of identifiers for bound variables,
   17.28 +which can then be used to match arbitrary subterms inside abstractions.
   17.29  *)
   17.30  
   17.31 -signature REWRITE1 = sig
   17.32 -  val setup : theory -> theory
   17.33 +signature REWRITE =
   17.34 +sig
   17.35 +  (* FIXME proper ML interface!? *)
   17.36  end
   17.37  
   17.38 -structure Rewrite : REWRITE1 =
   17.39 +structure Rewrite : REWRITE =
   17.40  struct
   17.41  
   17.42  datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list
   17.43 @@ -68,8 +70,10 @@
   17.44    let
   17.45      fun add_ident NONE _ l = l
   17.46        | add_ident (SOME name) ct l = (name, Thm.term_of ct) :: l
   17.47 -    fun inner rewr ctxt idents = CConv.abs_cconv (fn (ct, ctxt) => rewr ctxt (add_ident ident ct idents)) ctxt
   17.48 +    fun inner rewr ctxt idents =
   17.49 +      CConv.abs_cconv (fn (ct, ctxt) => rewr ctxt (add_ident ident ct idents)) ctxt
   17.50    in inner end
   17.51 +
   17.52  val fun_rewr_cconv : subterm_position = fn rewr => CConv.fun_cconv oo rewr
   17.53  val arg_rewr_cconv : subterm_position = fn rewr => CConv.arg_cconv oo rewr
   17.54  
   17.55 @@ -80,17 +84,19 @@
   17.56    case try (fastype_of #> dest_funT) u of
   17.57      NONE => raise TERM ("ft_abs: no function type", [u])
   17.58    | SOME (U, _) =>
   17.59 -  let
   17.60 -    val tyenv' = if T = dummyT then tyenv else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv
   17.61 -    val x = Free (the_default (Name.internal dummyN) s, Envir.norm_type tyenv' T)
   17.62 -    val eta_expand_cconv = CConv.rewr_cconv @{thm eta_expand}
   17.63 -    fun eta_expand rewr ctxt bounds = eta_expand_cconv then_conv rewr ctxt bounds
   17.64 -    val (u', pos') =
   17.65 -      case u of
   17.66 -        Abs (_,_,t') => (subst_bound (x, t'), pos o abs_rewr_cconv s)
   17.67 -      | _ => (u $ x, pos o eta_expand o abs_rewr_cconv s)
   17.68 -  in (tyenv', u', pos') end
   17.69 -  handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u])
   17.70 +      let
   17.71 +        val tyenv' =
   17.72 +          if T = dummyT then tyenv
   17.73 +          else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv
   17.74 +        val x = Free (the_default (Name.internal dummyN) s, Envir.norm_type tyenv' T)
   17.75 +        val eta_expand_cconv = CConv.rewr_cconv @{thm eta_expand}
   17.76 +        fun eta_expand rewr ctxt bounds = eta_expand_cconv then_conv rewr ctxt bounds
   17.77 +        val (u', pos') =
   17.78 +          case u of
   17.79 +            Abs (_,_,t') => (subst_bound (x, t'), pos o abs_rewr_cconv s)
   17.80 +          | _ => (u $ x, pos o eta_expand o abs_rewr_cconv s)
   17.81 +      in (tyenv', u', pos') end
   17.82 +      handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u])
   17.83  
   17.84  fun ft_fun _ (tyenv, l $ _, pos) = (tyenv, l, pos o fun_rewr_cconv)
   17.85    | ft_fun ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_fun ctxt o ft_abs ctxt (NONE, T)) ft
   17.86 @@ -127,7 +133,8 @@
   17.87            | (x :: xs) => (xs , desc o ft_all ctxt x)
   17.88          end
   17.89        | f rev_idents _ = (rev_idents, I)
   17.90 -  in case f (rev idents) t of
   17.91 +  in
   17.92 +    case f (rev idents) t of
   17.93        ([], ft') => SOME (ft' ft)
   17.94      | _ => NONE
   17.95    end
   17.96 @@ -143,7 +150,7 @@
   17.97    | _ => raise TERM ("ft_assm", [t])
   17.98  
   17.99  fun ft_judgment ctxt (ft as (_, t, _) : focusterm) =
  17.100 -  if Object_Logic.is_judgment (Proof_Context.theory_of ctxt) t
  17.101 +  if Object_Logic.is_judgment ctxt t
  17.102    then ft_arg ctxt ft
  17.103    else ft
  17.104  
  17.105 @@ -153,7 +160,8 @@
  17.106  fun find_subterms ctxt condition (ft as (_, t, _) : focusterm) =
  17.107    let
  17.108      val recurse = find_subterms ctxt condition
  17.109 -    val recursive_matches = case t of
  17.110 +    val recursive_matches =
  17.111 +      case t of
  17.112          _ $ _ => Seq.append (ft |> ft_fun ctxt |> recurse) (ft |> ft_arg ctxt |> recurse)
  17.113        | Abs (_,T,_) => ft |> ft_abs ctxt (NONE, T) |> recurse
  17.114        | _ => Seq.empty
  17.115 @@ -250,7 +258,6 @@
  17.116      fun apply_pats ft = ft
  17.117        |> Seq.single
  17.118        |> fold apply_pat pattern_list
  17.119 -
  17.120    in
  17.121      apply_pats
  17.122    end
  17.123 @@ -322,9 +329,9 @@
  17.124      val tac = rewrite_goal_with_thm ctxt pattern thms'
  17.125    in tac end
  17.126  
  17.127 -val setup =
  17.128 +val _ =
  17.129 +  Theory.setup
  17.130    let
  17.131 -
  17.132      fun mk_fix s = (Binding.name s, NONE, NoSyn)
  17.133  
  17.134      val raw_pattern : (string, binding * string option * mixfix) pattern list parser =
  17.135 @@ -342,11 +349,11 @@
  17.136  
  17.137        in Scan.repeat sep_atom >> (flat #> rev #> append_default) end
  17.138  
  17.139 -    fun ctxt_lift (scan : 'a parser) f = fn (ctxt : Context.generic, toks) =>
  17.140 +    fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) =>
  17.141        let
  17.142          val (r, toks') = scan toks
  17.143 -        val (r', ctxt') = Context.map_proof_result (fn ctxt => f ctxt r) ctxt
  17.144 -      in (r', (ctxt', toks' : Token.T list))end
  17.145 +        val (r', context') = Context.map_proof_result (fn ctxt => f ctxt r) context
  17.146 +      in (r', (context', toks' : Token.T list)) end
  17.147  
  17.148      fun read_fixes fixes ctxt =
  17.149        let fun read_typ (b, rawT, mx) = (b, Option.map (Syntax.read_typ ctxt) rawT, mx)
  17.150 @@ -354,7 +361,6 @@
  17.151  
  17.152      fun prep_pats ctxt (ps : (string, binding * string option * mixfix) pattern list) =
  17.153        let
  17.154 -
  17.155          fun add_constrs ctxt n (Abs (x, T, t)) =
  17.156              let
  17.157                val (x', ctxt') = yield_singleton Proof_Context.add_fixes (mk_fix x) ctxt
  17.158 @@ -470,10 +476,11 @@
  17.159  
  17.160      val subst_parser =
  17.161        let val scan = raw_pattern -- to_parser -- Parse.xthms1
  17.162 -      in ctxt_lift scan prep_args end
  17.163 +      in context_lift scan prep_args end
  17.164    in
  17.165      Method.setup @{binding rewrite} (subst_parser >>
  17.166 -      (fn (pattern, inthms, inst) => fn ctxt => SIMPLE_METHOD' (rewrite_tac ctxt (pattern, inst) inthms)))
  17.167 +      (fn (pattern, inthms, inst) => fn ctxt =>
  17.168 +        SIMPLE_METHOD' (rewrite_tac ctxt (pattern, inst) inthms)))
  17.169        "single-step rewriting, allowing subterm selection via patterns."
  17.170    end
  17.171  end
    18.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Apr 08 19:24:32 2015 +0200
    18.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Apr 08 22:15:03 2015 +0200
    18.3 @@ -321,7 +321,7 @@
    18.4            Config.put Quickcheck.finite_types true #>
    18.5            Config.put Quickcheck.finite_type_size 1 #>
    18.6            Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
    18.7 -        (false, false) [])) (map (rpair [] o Object_Logic.atomize_term thy)
    18.8 +        (false, false) [])) (map (rpair [] o Object_Logic.atomize_term ctxt)
    18.9          (fst (Variable.import_terms true [t] ctxt)))
   18.10    end
   18.11  
    19.1 --- a/src/HOL/Nitpick_Examples/minipick.ML	Wed Apr 08 19:24:32 2015 +0200
    19.2 +++ b/src/HOL/Nitpick_Examples/minipick.ML	Wed Apr 08 22:15:03 2015 +0200
    19.3 @@ -409,7 +409,7 @@
    19.4        | concrete (Type (@{type_name prod}, Ts)) = forall concrete Ts
    19.5        | concrete _ = true
    19.6      val neg_t =
    19.7 -      @{const Not} $ Object_Logic.atomize_term thy t
    19.8 +      @{const Not} $ Object_Logic.atomize_term ctxt t
    19.9        |> map_types unsetify_type
   19.10      val _ = fold_types (K o check_type ctxt raw_infinite) neg_t ()
   19.11      val frees = Term.add_frees neg_t []
    20.1 --- a/src/HOL/Nominal/nominal_induct.ML	Wed Apr 08 19:24:32 2015 +0200
    20.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Wed Apr 08 22:15:03 2015 +0200
    20.3 @@ -93,7 +93,7 @@
    20.4  
    20.5      fun rule_cases ctxt r =
    20.6        let val r' = if simp then Induct.simplified_rule ctxt r else r
    20.7 -      in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end;
    20.8 +      in Rule_Cases.make_nested ctxt (Thm.prop_of r') (Induct.rulified_term ctxt r') end;
    20.9    in
   20.10      (fn i => fn st =>
   20.11        rules
    21.1 --- a/src/HOL/Probability/Giry_Monad.thy	Wed Apr 08 19:24:32 2015 +0200
    21.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Wed Apr 08 22:15:03 2015 +0200
    21.3 @@ -324,7 +324,7 @@
    21.4    finally show ?thesis .
    21.5  qed
    21.6  
    21.7 -(* TODO: Rename. This name is too general – Manuel *)
    21.8 +(* TODO: Rename. This name is too general -- Manuel *)
    21.9  lemma measurable_pair_measure:
   21.10    assumes f: "f \<in> measurable M (subprob_algebra N)"
   21.11    assumes g: "g \<in> measurable M (subprob_algebra L)"
    22.1 --- a/src/HOL/ROOT	Wed Apr 08 19:24:32 2015 +0200
    22.2 +++ b/src/HOL/ROOT	Wed Apr 08 22:15:03 2015 +0200
    22.3 @@ -31,6 +31,7 @@
    22.4    *}
    22.5    theories
    22.6      Library
    22.7 +    Rewrite
    22.8      (*conflicting type class instantiations*)
    22.9      List_lexord
   22.10      Sublist_Order
    23.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Apr 08 19:24:32 2015 +0200
    23.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Apr 08 22:15:03 2015 +0200
    23.3 @@ -1243,10 +1243,9 @@
    23.4  
    23.5  fun presimp_prop ctxt type_enc t =
    23.6    let
    23.7 -    val thy = Proof_Context.theory_of ctxt
    23.8      val t = t |> Envir.beta_eta_contract
    23.9                |> transform_elim_prop
   23.10 -              |> Object_Logic.atomize_term thy
   23.11 +              |> Object_Logic.atomize_term ctxt
   23.12      val need_trueprop = (fastype_of t = @{typ bool})
   23.13      val is_ho = is_type_enc_higher_order type_enc
   23.14    in
    24.1 --- a/src/HOL/Tools/ATP/atp_waldmeister.ML	Wed Apr 08 19:24:32 2015 +0200
    24.2 +++ b/src/HOL/Tools/ATP/atp_waldmeister.ML	Wed Apr 08 22:15:03 2015 +0200
    24.3 @@ -445,7 +445,7 @@
    24.4    let
    24.5      val thy = Proof_Context.theory_of ctxt
    24.6  
    24.7 -    val preproc = Object_Logic.atomize_term thy
    24.8 +    val preproc = Object_Logic.atomize_term ctxt
    24.9  
   24.10      val conditions = map preproc hyps_t0
   24.11      val consequence = preproc concl_t0
    25.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Wed Apr 08 19:24:32 2015 +0200
    25.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Wed Apr 08 22:15:03 2015 +0200
    25.3 @@ -188,14 +188,12 @@
    25.4  
    25.5  fun mk_ind_goal ctxt branches =
    25.6    let
    25.7 -    val thy = Proof_Context.theory_of ctxt
    25.8 -
    25.9      fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
   25.10        HOLogic.mk_Trueprop (list_comb (P, map Free xs))
   25.11        |> fold_rev (curry Logic.mk_implies) Cs
   25.12        |> fold_rev (Logic.all o Free) ws
   25.13        |> term_conv ctxt (ind_atomize ctxt)
   25.14 -      |> Object_Logic.drop_judgment thy
   25.15 +      |> Object_Logic.drop_judgment ctxt
   25.16        |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
   25.17    in
   25.18      Sum_Tree.mk_sumcases HOLogic.boolT (map brnch branches)
    26.1 --- a/src/HOL/Tools/Function/relation.ML	Wed Apr 08 19:24:32 2015 +0200
    26.2 +++ b/src/HOL/Tools/Function/relation.ML	Wed Apr 08 22:15:03 2015 +0200
    26.3 @@ -10,40 +10,42 @@
    26.4    val relation_infer_tac: Proof.context -> term -> int -> tactic
    26.5  end
    26.6  
    26.7 -structure Function_Relation : FUNCTION_RELATION =
    26.8 +structure Function_Relation: FUNCTION_RELATION =
    26.9  struct
   26.10  
   26.11  (* tactic version *)
   26.12  
   26.13 -fun inst_state_tac ctxt inst st =
   26.14 -  (case Term.add_vars (Thm.prop_of st) [] of  (* FIXME tactic should not inspect main conclusion *)
   26.15 -    [v as (_, T)] =>
   26.16 -      PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt (inst T))])) st
   26.17 -  | _ => Seq.empty);
   26.18 +fun inst_state_tac ctxt inst =
   26.19 +  SUBGOAL (fn (goal, _) =>
   26.20 +    (case Term.add_vars goal [] of
   26.21 +      [v as (_, T)] =>
   26.22 +        PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt (inst T))]))
   26.23 +    | _ => no_tac));
   26.24  
   26.25  fun relation_tac ctxt rel i =
   26.26    TRY (Function_Common.termination_rule_tac ctxt i)
   26.27 -  THEN inst_state_tac ctxt rel;
   26.28 +  THEN inst_state_tac ctxt rel i;
   26.29  
   26.30  
   26.31  (* version with type inference *)
   26.32  
   26.33 -fun inst_state_infer_tac ctxt rel st =
   26.34 -  (case Term.add_vars (Thm.prop_of st) [] of  (* FIXME tactic should not inspect main conclusion *)
   26.35 -    [v as (_, T)] =>
   26.36 -      let
   26.37 -        val rel' = singleton (Variable.polymorphic ctxt) rel
   26.38 -          |> map_types Type_Infer.paramify_vars
   26.39 -          |> Type.constraint T
   26.40 -          |> Syntax.check_term ctxt
   26.41 -          |> Thm.cterm_of ctxt;
   26.42 -      in
   26.43 -        PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), rel')])) st
   26.44 -      end
   26.45 -  | _ => Seq.empty);
   26.46 +fun inst_state_infer_tac ctxt rel =
   26.47 +  SUBGOAL (fn (goal, _) =>
   26.48 +    (case Term.add_vars goal [] of
   26.49 +      [v as (_, T)] =>
   26.50 +        let
   26.51 +          val rel' =
   26.52 +            singleton (Variable.polymorphic ctxt) rel
   26.53 +            |> map_types Type_Infer.paramify_vars
   26.54 +            |> Type.constraint T
   26.55 +            |> Syntax.check_term ctxt;
   26.56 +        in
   26.57 +          PRIMITIVE (Thm.instantiate ([], [(Thm.cterm_of ctxt (Var v), Thm.cterm_of ctxt rel')]))
   26.58 +        end
   26.59 +    | _ => no_tac));
   26.60  
   26.61  fun relation_infer_tac ctxt rel i =
   26.62    TRY (Function_Common.termination_rule_tac ctxt i)
   26.63 -  THEN inst_state_infer_tac ctxt rel;
   26.64 +  THEN inst_state_infer_tac ctxt rel i;
   26.65  
   26.66  end
    27.1 --- a/src/HOL/Tools/Function/termination.ML	Wed Apr 08 19:24:32 2015 +0200
    27.2 +++ b/src/HOL/Tools/Function/termination.ML	Wed Apr 08 22:15:03 2015 +0200
    27.3 @@ -32,8 +32,6 @@
    27.4    val decompose_tac : Proof.context -> ttac
    27.5  end
    27.6  
    27.7 -
    27.8 -
    27.9  structure Termination : TERMINATION =
   27.10  struct
   27.11  
   27.12 @@ -275,14 +273,13 @@
   27.13  
   27.14  fun wf_union_tac ctxt st = SUBGOAL (fn _ =>
   27.15    let
   27.16 -    val thy = Proof_Context.theory_of ctxt
   27.17      val ((_ $ (_ $ rel)) :: ineqs) = Thm.prems_of st
   27.18  
   27.19      fun mk_compr ineq =
   27.20        let
   27.21          val (vars, prems, lhs, rhs) = dest_term ineq
   27.22        in
   27.23 -        mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (Object_Logic.atomize_term thy) prems)
   27.24 +        mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (Object_Logic.atomize_term ctxt) prems)
   27.25        end
   27.26  
   27.27      val relation =
   27.28 @@ -360,5 +357,4 @@
   27.29      else solve_trivial_tac D i
   27.30    end)
   27.31  
   27.32 -
   27.33  end
    28.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 08 19:24:32 2015 +0200
    28.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Apr 08 22:15:03 2015 +0200
    28.3 @@ -300,7 +300,7 @@
    28.4      val psimp_table = const_psimp_table ctxt subst
    28.5      val choice_spec_table = const_choice_spec_table ctxt subst
    28.6      val nondefs =
    28.7 -      nondefs |> filter_out (is_choice_spec_axiom thy choice_spec_table)
    28.8 +      nondefs |> filter_out (is_choice_spec_axiom ctxt choice_spec_table)
    28.9      val intro_table = inductive_intro_table ctxt subst def_tables
   28.10      val ground_thm_table = ground_theorem_table thy
   28.11      val ersatz_table = ersatz_table ctxt
    29.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Apr 08 19:24:32 2015 +0200
    29.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Apr 08 22:15:03 2015 +0200
    29.3 @@ -218,7 +218,7 @@
    29.4    val nondef_props_for_const :
    29.5      theory -> bool -> const_table -> string * typ -> term list
    29.6    val is_choice_spec_fun : hol_context -> string * typ -> bool
    29.7 -  val is_choice_spec_axiom : theory -> const_table -> term -> bool
    29.8 +  val is_choice_spec_axiom : Proof.context -> const_table -> term -> bool
    29.9    val is_raw_equational_fun : hol_context -> string * typ -> bool
   29.10    val is_equational_fun : hol_context -> string * typ -> bool
   29.11    val codatatype_bisim_axioms : hol_context -> typ -> term list
   29.12 @@ -1548,13 +1548,13 @@
   29.13    | unvarify_term (Abs (s, T, t')) = Abs (s, T, unvarify_term t')
   29.14    | unvarify_term t = t
   29.15  
   29.16 -fun axiom_for_choice_spec thy =
   29.17 +fun axiom_for_choice_spec ctxt =
   29.18    unvarify_term
   29.19 -  #> Object_Logic.atomize_term thy
   29.20 +  #> Object_Logic.atomize_term ctxt
   29.21    #> Choice_Specification.close_form
   29.22    #> HOLogic.mk_Trueprop
   29.23  
   29.24 -fun is_choice_spec_fun ({thy, def_tables, nondef_table, choice_spec_table, ...}
   29.25 +fun is_choice_spec_fun ({thy, ctxt, def_tables, nondef_table, choice_spec_table, ...}
   29.26                          : hol_context) x =
   29.27    case nondef_props_for_const thy true choice_spec_table x of
   29.28      [] => false
   29.29 @@ -1565,7 +1565,7 @@
   29.30              let val ts' = nondef_props_for_const thy true nondef_table x in
   29.31                length ts' = length ts andalso
   29.32                forall (fn t =>
   29.33 -                         exists (curry (op aconv) (axiom_for_choice_spec thy t))
   29.34 +                         exists (curry (op aconv) (axiom_for_choice_spec ctxt t))
   29.35                                  ts') ts
   29.36              end
   29.37  
   29.38 @@ -2074,10 +2074,10 @@
   29.39  
   29.40  exception NO_TRIPLE of unit
   29.41  
   29.42 -fun triple_for_intro_rule thy x t =
   29.43 +fun triple_for_intro_rule ctxt x t =
   29.44    let
   29.45 -    val prems = Logic.strip_imp_prems t |> map (Object_Logic.atomize_term thy)
   29.46 -    val concl = Logic.strip_imp_concl t |> Object_Logic.atomize_term thy
   29.47 +    val prems = Logic.strip_imp_prems t |> map (Object_Logic.atomize_term ctxt)
   29.48 +    val concl = Logic.strip_imp_concl t |> Object_Logic.atomize_term ctxt
   29.49      val (main, side) = List.partition (exists_Const (curry (op =) x)) prems
   29.50      val is_good_head = curry (op =) (Const x) o head_of
   29.51    in
   29.52 @@ -2122,7 +2122,7 @@
   29.53      [] => raise TERM ("Nitpick_HOL.uncached_is_well_founded_inductive",
   29.54                        [Const x])
   29.55    | intro_ts =>
   29.56 -    (case map (triple_for_intro_rule thy x) intro_ts
   29.57 +    (case map (triple_for_intro_rule ctxt x) intro_ts
   29.58            |> filter_out (null o #2) of
   29.59         [] => true
   29.60       | triples =>
   29.61 @@ -2149,7 +2149,7 @@
   29.62             SOME wf => wf
   29.63           | NONE =>
   29.64             let
   29.65 -             val goal = prop |> Thm.global_cterm_of thy |> Goal.init
   29.66 +             val goal = prop |> Thm.cterm_of ctxt |> Goal.init
   29.67               val wf = exists (terminates_by ctxt tac_timeout goal)
   29.68                               termination_tacs
   29.69             in Synchronized.change cached_wf_props (cons (prop, wf)); wf end
    30.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Apr 08 19:24:32 2015 +0200
    30.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Apr 08 22:15:03 2015 +0200
    30.3 @@ -1050,7 +1050,7 @@
    30.4      fun try_out negate =
    30.5        let
    30.6          val concl = (negate ? curry (op $) @{const Not})
    30.7 -                    (Object_Logic.atomize_term thy prop)
    30.8 +                    (Object_Logic.atomize_term ctxt prop)
    30.9          val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl))
   30.10                     |> map_types (map_type_tfree
   30.11                                       (fn (s, []) => TFree (s, @{sort type})
   30.12 @@ -1062,7 +1062,7 @@
   30.13              |> writeln
   30.14            else
   30.15              ()
   30.16 -        val goal = prop |> Thm.global_cterm_of thy |> Goal.init
   30.17 +        val goal = prop |> Thm.cterm_of ctxt |> Goal.init
   30.18        in
   30.19          (goal |> SINGLE (DETERM_TIMEOUT auto_timeout (auto_tac ctxt))
   30.20                |> the |> Goal.finish ctxt; true)
    31.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Apr 08 19:24:32 2015 +0200
    31.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Apr 08 22:15:03 2015 +0200
    31.3 @@ -236,7 +236,7 @@
    31.4      val rewrs = map (swap o dest) @{thms all_simps} @
    31.5        (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff},
    31.6          @{thm bot_fun_def}, @{thm less_bool_def}])
    31.7 -    val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term thy t)
    31.8 +    val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term ctxt t)
    31.9      val (vs, body) = strip_all t'
   31.10      val vs' = Variable.variant_frees ctxt [t'] vs
   31.11    in
    32.1 --- a/src/HOL/Tools/SMT/smtlib_isar.ML	Wed Apr 08 19:24:32 2015 +0200
    32.2 +++ b/src/HOL/Tools/SMT/smtlib_isar.ML	Wed Apr 08 22:15:03 2015 +0200
    32.3 @@ -44,7 +44,7 @@
    32.4  fun postprocess_step_conclusion ctxt rewrite_rules ll_defs =
    32.5    let val thy = Proof_Context.theory_of ctxt in
    32.6      Raw_Simplifier.rewrite_term thy rewrite_rules []
    32.7 -    #> Object_Logic.atomize_term thy
    32.8 +    #> Object_Logic.atomize_term ctxt
    32.9      #> not (null ll_defs) ? unlift_term ll_defs
   32.10      #> simplify_bool
   32.11      #> unskolemize_names ctxt
    33.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Apr 08 19:24:32 2015 +0200
    33.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Apr 08 22:15:03 2015 +0200
    33.3 @@ -428,10 +428,9 @@
    33.4  fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
    33.5    if Config.get ctxt instantiate_inducts then
    33.6      let
    33.7 -      val thy = Proof_Context.theory_of ctxt
    33.8        val ind_stmt =
    33.9          (hyp_ts |> filter_out (null o external_frees), concl_t)
   33.10 -        |> Logic.list_implies |> Object_Logic.atomize_term thy
   33.11 +        |> Logic.list_implies |> Object_Logic.atomize_term ctxt
   33.12        val ind_stmt_xs = external_frees ind_stmt
   33.13      in
   33.14        maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
    34.1 --- a/src/HOL/Tools/coinduction.ML	Wed Apr 08 19:24:32 2015 +0200
    34.2 +++ b/src/HOL/Tools/coinduction.ML	Wed Apr 08 22:15:03 2015 +0200
    34.3 @@ -37,7 +37,7 @@
    34.4      (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o eresolve0_tac [thin_rl])) i st
    34.5    end;
    34.6  
    34.7 -fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _, _) =>
    34.8 +fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _) =>
    34.9    let
   34.10      val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
   34.11      fun find_coinduct t =
   34.12 @@ -98,9 +98,9 @@
   34.13                 DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
   34.14                   (case prems of
   34.15                     [] => all_tac
   34.16 -                 | inv::case_prems =>
   34.17 +                 | inv :: case_prems =>
   34.18                       let
   34.19 -                       val (init, last) = funpow_yield (p + e - 1) HOLogic.conj_elim inv;
   34.20 +                       val (init, last) = funpow_yield (p + e - 1) (HOLogic.conj_elim ctxt) inv;
   34.21                         val inv_thms = init @ [last];
   34.22                         val eqs = take e inv_thms;
   34.23                         fun is_local_var t =
   34.24 @@ -115,7 +115,7 @@
   34.25          end) ctxt) THEN'
   34.26        K (prune_params_tac ctxt))
   34.27      #> Seq.maps (fn st =>
   34.28 -      CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt, Thm.prop_of st) cases) all_tac st)
   34.29 +      CASES (Rule_Cases.make_common ctxt (Thm.prop_of st) cases) all_tac st)
   34.30    end));
   34.31  
   34.32  local
    35.1 --- a/src/HOL/Tools/groebner.ML	Wed Apr 08 19:24:32 2015 +0200
    35.2 +++ b/src/HOL/Tools/groebner.ML	Wed Apr 08 22:15:03 2015 +0200
    35.3 @@ -677,13 +677,13 @@
    35.4  fun refute ctxt tm =
    35.5   if tm aconvc false_tm then assume_Trueprop tm else
    35.6   ((let
    35.7 -   val (nths0,eths0) = List.partition (is_neg o concl) (HOLogic.conj_elims (assume_Trueprop tm))
    35.8 +   val (nths0,eths0) = List.partition (is_neg o concl) (HOLogic.conj_elims ctxt (assume_Trueprop tm))
    35.9     val  nths = filter (is_eq o Thm.dest_arg o concl) nths0
   35.10     val eths = filter (is_eq o concl) eths0
   35.11    in
   35.12     if null eths then
   35.13      let
   35.14 -      val th1 = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr th1 th2)) nths
   35.15 +      val th1 = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr ctxt th1 th2)) nths
   35.16        val th2 =
   35.17          Conv.fconv_rule
   35.18            ((Conv.arg_conv #> Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) th1
   35.19 @@ -703,13 +703,13 @@
   35.20        end
   35.21       else
   35.22        let
   35.23 -       val nth = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr th1 th2)) nths
   35.24 +       val nth = end_itlist (fn th1 => fn th2 => idom_rule ctxt (HOLogic.conj_intr ctxt th1 th2)) nths
   35.25         val (vars,pol::pols) =
   35.26            grobify_equations(list_mk_conj(Thm.dest_arg(concl nth)::map concl eths))
   35.27         val (deg,l,cert) = grobner_strong vars pols pol
   35.28         val th1 =
   35.29          Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) nth
   35.30 -       val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr th1) neq_01
   35.31 +       val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr ctxt th1) neq_01
   35.32        in (vars,l,cert,th2)
   35.33        end)
   35.34      val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c >/ rat_0) p)) cert
   35.35 @@ -724,7 +724,7 @@
   35.36                (nth eths i |> mk_meta_eq)) pols)
   35.37      val th1 = thm_fn herts_pos
   35.38      val th2 = thm_fn herts_neg
   35.39 -    val th3 = HOLogic.conj_intr(mk_add (Thm.symmetric th1) th2 |> mk_object_eq) noteqth
   35.40 +    val th3 = HOLogic.conj_intr ctxt (mk_add (Thm.symmetric th1) th2 |> mk_object_eq) noteqth
   35.41      val th4 =
   35.42        Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv o Conv.binop_conv) ring_normalize_conv)
   35.43          (neq_rule l th3)
   35.44 @@ -931,7 +931,7 @@
   35.45    Object_Logic.full_atomize_tac ctxt
   35.46    THEN' presimplify ctxt add_ths del_ths
   35.47    THEN' CSUBGOAL (fn (p, i) =>
   35.48 -    rtac (let val form = Object_Logic.dest_judgment p
   35.49 +    rtac (let val form = Object_Logic.dest_judgment ctxt p
   35.50            in case get_ring_ideal_convs ctxt form of
   35.51             NONE => Thm.reflexive form
   35.52            | SOME thy => #ring_conv thy ctxt form
    36.1 --- a/src/HOL/Tools/hologic.ML	Wed Apr 08 19:24:32 2015 +0200
    36.2 +++ b/src/HOL/Tools/hologic.ML	Wed Apr 08 22:15:03 2015 +0200
    36.3 @@ -24,9 +24,9 @@
    36.4    val mk_set: typ -> term list -> term
    36.5    val dest_set: term -> term list
    36.6    val mk_UNIV: typ -> term
    36.7 -  val conj_intr: thm -> thm -> thm
    36.8 -  val conj_elim: thm -> thm * thm
    36.9 -  val conj_elims: thm -> thm list
   36.10 +  val conj_intr: Proof.context -> thm -> thm -> thm
   36.11 +  val conj_elim: Proof.context -> thm -> thm * thm
   36.12 +  val conj_elims: Proof.context -> thm -> thm list
   36.13    val conj: term
   36.14    val disj: term
   36.15    val imp: term
   36.16 @@ -203,25 +203,25 @@
   36.17    | _ => raise CTERM ("Trueprop_conv", [ct]))
   36.18  
   36.19  
   36.20 -fun conj_intr thP thQ =
   36.21 +fun conj_intr ctxt thP thQ =
   36.22    let
   36.23 -    val (P, Q) = apply2 (Object_Logic.dest_judgment o Thm.cprop_of) (thP, thQ)
   36.24 +    val (P, Q) = apply2 (Object_Logic.dest_judgment ctxt o Thm.cprop_of) (thP, thQ)
   36.25        handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
   36.26      val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
   36.27    in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end;
   36.28  
   36.29 -fun conj_elim thPQ =
   36.30 +fun conj_elim ctxt thPQ =
   36.31    let
   36.32 -    val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment (Thm.cprop_of thPQ))
   36.33 +    val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment ctxt (Thm.cprop_of thPQ))
   36.34        handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
   36.35      val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
   36.36      val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ;
   36.37      val thQ = Thm.implies_elim (inst @{thm conjunct2}) thPQ;
   36.38    in (thP, thQ) end;
   36.39  
   36.40 -fun conj_elims th =
   36.41 -  let val (th1, th2) = conj_elim th
   36.42 -  in conj_elims th1 @ conj_elims th2 end handle THM _ => [th];
   36.43 +fun conj_elims ctxt th =
   36.44 +  let val (th1, th2) = conj_elim ctxt th
   36.45 +  in conj_elims ctxt th1 @ conj_elims ctxt th2 end handle THM _ => [th];
   36.46  
   36.47  val conj = @{term HOL.conj}
   36.48  and disj = @{term HOL.disj}
    37.1 --- a/src/HOL/Tools/simpdata.ML	Wed Apr 08 19:24:32 2015 +0200
    37.2 +++ b/src/HOL/Tools/simpdata.ML	Wed Apr 08 22:15:03 2015 +0200
    37.3 @@ -147,7 +147,7 @@
    37.4  
    37.5  structure Splitter = Splitter
    37.6  (
    37.7 -  val thy = @{theory}
    37.8 +  val context = @{context}
    37.9    val mk_eq = mk_eq
   37.10    val meta_eq_to_iff = @{thm meta_eq_to_obj_eq}
   37.11    val iffD = @{thm iffD2}
    38.1 --- a/src/HOL/Topological_Spaces.thy	Wed Apr 08 19:24:32 2015 +0200
    38.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Apr 08 22:15:03 2015 +0200
    38.3 @@ -443,23 +443,22 @@
    38.4  qed
    38.5  
    38.6  ML {*
    38.7 -  fun eventually_elim_tac ctxt thms = SUBGOAL_CASES (fn (_, _, st) =>
    38.8 +  fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
    38.9      let
   38.10 -      val thy = Proof_Context.theory_of ctxt
   38.11 -      val mp_thms = thms RL [@{thm eventually_rev_mp}]
   38.12 +      val mp_thms = facts RL @{thms eventually_rev_mp}
   38.13        val raw_elim_thm =
   38.14          (@{thm allI} RS @{thm always_eventually})
   38.15          |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
   38.16 -        |> fold (fn _ => fn thm => @{thm impI} RS thm) thms
   38.17 -      val cases_prop = Thm.prop_of (raw_elim_thm RS st)
   38.18 -      val cases = (Rule_Cases.make_common (thy, cases_prop) [(("elim", []), [])])
   38.19 +        |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
   38.20 +      val cases_prop = Thm.prop_of (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal))
   38.21 +      val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
   38.22      in
   38.23 -      CASES cases (rtac raw_elim_thm 1)
   38.24 -    end) 1
   38.25 +      CASES cases (rtac raw_elim_thm i)
   38.26 +    end)
   38.27  *}
   38.28  
   38.29  method_setup eventually_elim = {*
   38.30 -  Scan.succeed (fn ctxt => METHOD_CASES (eventually_elim_tac ctxt))
   38.31 +  Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
   38.32  *} "elimination of eventually quantifiers"
   38.33  
   38.34  
    39.1 --- a/src/Provers/classical.ML	Wed Apr 08 19:24:32 2015 +0200
    39.2 +++ b/src/Provers/classical.ML	Wed Apr 08 22:15:03 2015 +0200
    39.3 @@ -72,7 +72,7 @@
    39.4    val deepen_tac: Proof.context -> int -> int -> tactic
    39.5  
    39.6    val contr_tac: Proof.context -> int -> tactic
    39.7 -  val dup_elim: Context.generic option -> thm -> thm
    39.8 +  val dup_elim: Proof.context -> thm -> thm
    39.9    val dup_intr: thm -> thm
   39.10    val dup_step_tac: Proof.context -> int -> tactic
   39.11    val eq_mp_tac: Proof.context -> int -> tactic
   39.12 @@ -96,7 +96,7 @@
   39.13  signature CLASSICAL =
   39.14  sig
   39.15    include BASIC_CLASSICAL
   39.16 -  val classical_rule: thm -> thm
   39.17 +  val classical_rule: Proof.context -> thm -> thm
   39.18    type netpair = (int * (bool * thm)) Net.net * (int * (bool * thm)) Net.net
   39.19    val rep_cs: claset ->
   39.20     {safeIs: thm Item_Net.T,
   39.21 @@ -144,8 +144,8 @@
   39.22      [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W
   39.23  *)
   39.24  
   39.25 -fun classical_rule rule =
   39.26 -  if is_some (Object_Logic.elim_concl rule) then
   39.27 +fun classical_rule ctxt rule =
   39.28 +  if is_some (Object_Logic.elim_concl ctxt rule) then
   39.29      let
   39.30        val rule' = rule RS Data.classical;
   39.31        val concl' = Thm.concl_of rule';
   39.32 @@ -165,13 +165,8 @@
   39.33    else rule;
   39.34  
   39.35  (*flatten nested meta connectives in prems*)
   39.36 -fun flat_rule opt_context th =
   39.37 -  let
   39.38 -    val ctxt =
   39.39 -      (case opt_context of
   39.40 -        NONE => Proof_Context.init_global (Thm.theory_of_thm th)
   39.41 -      | SOME context => Context.proof_of context);
   39.42 -  in Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt)) th end;
   39.43 +fun flat_rule ctxt =
   39.44 +  Conv.fconv_rule (Conv.prems_conv ~1 (Object_Logic.atomize_prems ctxt));
   39.45  
   39.46  
   39.47  (*** Useful tactics for classical reasoning ***)
   39.48 @@ -206,13 +201,8 @@
   39.49  (*Duplication of hazardous rules, for complete provers*)
   39.50  fun dup_intr th = zero_var_indexes (th RS Data.classical);
   39.51  
   39.52 -fun dup_elim context th =
   39.53 -  let
   39.54 -    val ctxt =
   39.55 -      (case context of
   39.56 -        SOME c => Context.proof_of c
   39.57 -      | NONE => Proof_Context.init_global (Thm.theory_of_thm th));
   39.58 -    val rl = (th RSN (2, revcut_rl)) |> Thm.assumption (SOME ctxt) 2 |> Seq.hd;
   39.59 +fun dup_elim ctxt th =
   39.60 +  let val rl = (th RSN (2, revcut_rl)) |> Thm.assumption (SOME ctxt) 2 |> Seq.hd;
   39.61    in rule_by_tactic ctxt (TRYALL (eresolve_tac ctxt [revcut_rl])) rl end;
   39.62  
   39.63  
   39.64 @@ -259,6 +249,9 @@
   39.65      In case of overlap, new rules are tried BEFORE old ones!!
   39.66  ***)
   39.67  
   39.68 +fun default_context (SOME context) _ = Context.proof_of context
   39.69 +  | default_context NONE th = Proof_Context.init_global (Thm.theory_of_thm th);
   39.70 +
   39.71  (*For use with biresolve_tac.  Combines intro rules with swap to handle negated
   39.72    assumptions.  Pairs elim rules with true. *)
   39.73  fun joinrules (intrs, elims) =
   39.74 @@ -320,7 +313,8 @@
   39.75    if warn_rules context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
   39.76    else
   39.77      let
   39.78 -      val th' = flat_rule context th;
   39.79 +      val ctxt = default_context context th;
   39.80 +      val th' = flat_rule ctxt th;
   39.81        val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   39.82          List.partition Thm.no_prems [th'];
   39.83        val nI = Item_Net.length safeIs + 1;
   39.84 @@ -349,7 +343,8 @@
   39.85      error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
   39.86    else
   39.87      let
   39.88 -      val th' = classical_rule (flat_rule context th);
   39.89 +      val ctxt = default_context context th;
   39.90 +      val th' = classical_rule ctxt (flat_rule ctxt th);
   39.91        val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
   39.92          List.partition (fn rl => Thm.nprems_of rl=1) [th'];
   39.93        val nI = Item_Net.length safeIs;
   39.94 @@ -381,7 +376,8 @@
   39.95    if warn_rules context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
   39.96    else
   39.97      let
   39.98 -      val th' = flat_rule context th;
   39.99 +      val ctxt = default_context context th;
  39.100 +      val th' = flat_rule ctxt th;
  39.101        val nI = Item_Net.length hazIs + 1;
  39.102        val nE = Item_Net.length hazEs;
  39.103        val _ = warn_claset context th cs;
  39.104 @@ -410,7 +406,8 @@
  39.105      error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
  39.106    else
  39.107      let
  39.108 -      val th' = classical_rule (flat_rule context th);
  39.109 +      val ctxt = default_context context th;
  39.110 +      val th' = classical_rule ctxt (flat_rule ctxt th);
  39.111        val nI = Item_Net.length hazIs;
  39.112        val nE = Item_Net.length hazEs + 1;
  39.113        val _ = warn_claset context th cs;
  39.114 @@ -418,7 +415,7 @@
  39.115        CS
  39.116         {hazEs = Item_Net.update th hazEs,
  39.117          haz_netpair = insert (nI, nE) ([], [th']) haz_netpair,
  39.118 -        dup_netpair = insert (nI, nE) ([], [dup_elim context th']) dup_netpair,
  39.119 +        dup_netpair = insert (nI, nE) ([], [dup_elim ctxt th']) dup_netpair,
  39.120          safeIs = safeIs,
  39.121          safeEs = safeEs,
  39.122          hazIs = hazIs,
  39.123 @@ -443,7 +440,8 @@
  39.124        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
  39.125    if Item_Net.member safeIs th then
  39.126      let
  39.127 -      val th' = flat_rule context th;
  39.128 +      val ctxt = default_context context th;
  39.129 +      val th' = flat_rule ctxt th;
  39.130        val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'];
  39.131      in
  39.132        CS
  39.133 @@ -466,7 +464,8 @@
  39.134        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
  39.135    if Item_Net.member safeEs th then
  39.136      let
  39.137 -      val th' = classical_rule (flat_rule context th);
  39.138 +      val ctxt = default_context context th;
  39.139 +      val th' = classical_rule ctxt (flat_rule ctxt th);
  39.140        val (safe0_rls, safep_rls) = List.partition (fn rl => Thm.nprems_of rl = 1) [th'];
  39.141      in
  39.142        CS
  39.143 @@ -488,7 +487,10 @@
  39.144      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
  39.145        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
  39.146    if Item_Net.member hazIs th then
  39.147 -    let val th' = flat_rule context th in
  39.148 +    let
  39.149 +      val ctxt = default_context context th;
  39.150 +      val th' = flat_rule ctxt th;
  39.151 +    in
  39.152        CS
  39.153         {haz_netpair = delete ([th'], []) haz_netpair,
  39.154          dup_netpair = delete ([dup_intr th'], []) dup_netpair,
  39.155 @@ -510,10 +512,13 @@
  39.156      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
  39.157        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
  39.158    if Item_Net.member hazEs th then
  39.159 -    let val th' = classical_rule (flat_rule context th) in
  39.160 +    let
  39.161 +      val ctxt = default_context context th;
  39.162 +      val th' = classical_rule ctxt (flat_rule ctxt th);
  39.163 +    in
  39.164        CS
  39.165         {haz_netpair = delete ([], [th']) haz_netpair,
  39.166 -        dup_netpair = delete ([], [dup_elim context th']) dup_netpair,
  39.167 +        dup_netpair = delete ([], [dup_elim ctxt th']) dup_netpair,
  39.168          safeIs = safeIs,
  39.169          safeEs = safeEs,
  39.170          hazIs = hazIs,
    40.1 --- a/src/Provers/splitter.ML	Wed Apr 08 19:24:32 2015 +0200
    40.2 +++ b/src/Provers/splitter.ML	Wed Apr 08 22:15:03 2015 +0200
    40.3 @@ -9,7 +9,7 @@
    40.4  
    40.5  signature SPLITTER_DATA =
    40.6  sig
    40.7 -  val thy           : theory
    40.8 +  val context       : Proof.context
    40.9    val mk_eq         : thm -> thm
   40.10    val meta_eq_to_iff: thm (* "x == y ==> x = y"                      *)
   40.11    val iffD          : thm (* "[| P = Q; Q |] ==> P"                  *)
   40.12 @@ -43,14 +43,14 @@
   40.13  struct
   40.14  
   40.15  val Const (const_not, _) $ _ =
   40.16 -  Object_Logic.drop_judgment Data.thy
   40.17 +  Object_Logic.drop_judgment Data.context
   40.18      (#1 (Logic.dest_implies (Thm.prop_of Data.notnotD)));
   40.19  
   40.20  val Const (const_or , _) $ _ $ _ =
   40.21 -  Object_Logic.drop_judgment Data.thy
   40.22 +  Object_Logic.drop_judgment Data.context
   40.23      (#1 (Logic.dest_implies (Thm.prop_of Data.disjE)));
   40.24  
   40.25 -val const_Trueprop = Object_Logic.judgment_name Data.thy;
   40.26 +val const_Trueprop = Object_Logic.judgment_name Data.context;
   40.27  
   40.28  
   40.29  fun split_format_err () = error "Wrong format for split rule";
    41.1 --- a/src/Pure/Isar/auto_bind.ML	Wed Apr 08 19:24:32 2015 +0200
    41.2 +++ b/src/Pure/Isar/auto_bind.ML	Wed Apr 08 22:15:03 2015 +0200
    41.3 @@ -9,8 +9,8 @@
    41.4    val thesisN: string
    41.5    val thisN: string
    41.6    val assmsN: string
    41.7 -  val goal: theory -> term list -> (indexname * term option) list
    41.8 -  val facts: theory -> term list -> (indexname * term option) list
    41.9 +  val goal: Proof.context -> term list -> (indexname * term option) list
   41.10 +  val facts: Proof.context -> term list -> (indexname * term option) list
   41.11    val no_facts: (indexname * term option) list
   41.12  end;
   41.13  
   41.14 @@ -23,29 +23,29 @@
   41.15  val thisN = "this";
   41.16  val assmsN = "assms";
   41.17  
   41.18 -fun strip_judgment thy = Object_Logic.drop_judgment thy o Logic.strip_assums_concl;
   41.19 +fun strip_judgment ctxt = Object_Logic.drop_judgment ctxt o Logic.strip_assums_concl;
   41.20  
   41.21 -fun statement_binds thy name prop =
   41.22 -  [((name, 0), SOME (fold_rev Term.abs (Logic.strip_params prop) (strip_judgment thy prop)))];
   41.23 +fun statement_binds ctxt name prop =
   41.24 +  [((name, 0), SOME (fold_rev Term.abs (Logic.strip_params prop) (strip_judgment ctxt prop)))];
   41.25  
   41.26  
   41.27  (* goal *)
   41.28  
   41.29 -fun goal thy [prop] = statement_binds thy thesisN prop
   41.30 +fun goal ctxt [prop] = statement_binds ctxt thesisN prop
   41.31    | goal _ _ = [((thesisN, 0), NONE)];
   41.32  
   41.33  
   41.34  (* facts *)
   41.35  
   41.36 -fun get_arg thy prop =
   41.37 -  (case strip_judgment thy prop of
   41.38 +fun get_arg ctxt prop =
   41.39 +  (case strip_judgment ctxt prop of
   41.40      _ $ t => SOME (fold_rev Term.abs (Logic.strip_params prop) t)
   41.41    | _ => NONE);
   41.42  
   41.43  fun facts _ [] = []
   41.44 -  | facts thy props =
   41.45 +  | facts ctxt props =
   41.46        let val prop = List.last props
   41.47 -      in [(Syntax_Ext.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end;
   41.48 +      in [(Syntax_Ext.dddot_indexname, get_arg ctxt prop)] @ statement_binds ctxt thisN prop end;
   41.49  
   41.50  val no_facts = [(Syntax_Ext.dddot_indexname, NONE), ((thisN, 0), NONE)];
   41.51  
    42.1 --- a/src/Pure/Isar/element.ML	Wed Apr 08 19:24:32 2015 +0200
    42.2 +++ b/src/Pure/Isar/element.ML	Wed Apr 08 22:15:03 2015 +0200
    42.3 @@ -197,13 +197,12 @@
    42.4  
    42.5  local
    42.6  
    42.7 -fun standard_elim th =
    42.8 -  (case Object_Logic.elim_concl th of
    42.9 +fun standard_elim ctxt th =
   42.10 +  (case Object_Logic.elim_concl ctxt th of
   42.11      SOME C =>
   42.12        let
   42.13 -        val thy = Thm.theory_of_thm th;
   42.14          val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C);
   42.15 -        val th' = Thm.instantiate ([], [(Thm.global_cterm_of thy C, Thm.global_cterm_of thy thesis)]) th;
   42.16 +        val th' = Thm.instantiate ([], [apply2 (Thm.cterm_of ctxt) (C, thesis)]) th;
   42.17        in (th', true) end
   42.18    | NONE => (th, false));
   42.19  
   42.20 @@ -227,13 +226,11 @@
   42.21  
   42.22  fun pretty_statement ctxt kind raw_th =
   42.23    let
   42.24 -    val thy = Proof_Context.theory_of ctxt;
   42.25 -
   42.26 -    val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf ctxt raw_th);
   42.27 +    val (th, is_elim) = standard_elim ctxt (Raw_Simplifier.norm_hhf ctxt raw_th);
   42.28      val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body true ctxt);
   42.29      val prop = Thm.prop_of th';
   42.30      val (prems, concl) = Logic.strip_horn prop;
   42.31 -    val concl_term = Object_Logic.drop_judgment thy concl;
   42.32 +    val concl_term = Object_Logic.drop_judgment ctxt concl;
   42.33  
   42.34      val fixes = fold_aterms (fn v as Free (x, T) =>
   42.35          if Variable.is_newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
    43.1 --- a/src/Pure/Isar/expression.ML	Wed Apr 08 19:24:32 2015 +0200
    43.2 +++ b/src/Pure/Isar/expression.ML	Wed Apr 08 22:15:03 2015 +0200
    43.3 @@ -622,16 +622,15 @@
    43.4  
    43.5  val introN = "intro";
    43.6  
    43.7 -fun atomize_spec thy ts =
    43.8 +fun atomize_spec ctxt ts =
    43.9    let
   43.10      val t = Logic.mk_conjunction_balanced ts;
   43.11 -    val body = Object_Logic.atomize_term thy t;
   43.12 +    val body = Object_Logic.atomize_term ctxt t;
   43.13      val bodyT = Term.fastype_of body;
   43.14    in
   43.15      if bodyT = propT
   43.16 -    then (t, propT, Thm.reflexive (Thm.global_cterm_of thy t))
   43.17 -    else
   43.18 -      (body, bodyT, Object_Logic.atomize (Proof_Context.init_global thy) (Thm.global_cterm_of thy t))
   43.19 +    then (t, propT, Thm.reflexive (Thm.cterm_of ctxt t))
   43.20 +    else (body, bodyT, Object_Logic.atomize ctxt (Thm.cterm_of ctxt t))
   43.21    end;
   43.22  
   43.23  (* achieve plain syntax for locale predicates (without "PROP") *)
   43.24 @@ -658,7 +657,9 @@
   43.25    let
   43.26      val name = Sign.full_name thy binding;
   43.27  
   43.28 -    val (body, bodyT, body_eq) = atomize_spec thy norm_ts;
   43.29 +    val thy_ctxt = Proof_Context.init_global thy;
   43.30 +
   43.31 +    val (body, bodyT, body_eq) = atomize_spec thy_ctxt norm_ts;
   43.32      val env = Term.add_free_names body [];
   43.33      val xs = filter (member (op =) env o #1) parms;
   43.34      val Ts = map #2 xs;
   43.35 @@ -669,7 +670,7 @@
   43.36  
   43.37      val args = map Logic.mk_type extraTs @ map Free xs;
   43.38      val head = Term.list_comb (Const (name, predT), args);
   43.39 -    val statement = Object_Logic.ensure_propT thy head;
   43.40 +    val statement = Object_Logic.ensure_propT thy_ctxt head;
   43.41  
   43.42      val ([pred_def], defs_thy) =
   43.43        thy
    44.1 --- a/src/Pure/Isar/object_logic.ML	Wed Apr 08 19:24:32 2015 +0200
    44.2 +++ b/src/Pure/Isar/object_logic.ML	Wed Apr 08 22:15:03 2015 +0200
    44.3 @@ -6,26 +6,26 @@
    44.4  
    44.5  signature OBJECT_LOGIC =
    44.6  sig
    44.7 -  val get_base_sort: theory -> sort option
    44.8 +  val get_base_sort: Proof.context -> sort option
    44.9    val add_base_sort: sort -> theory -> theory
   44.10    val add_judgment: binding * typ * mixfix -> theory -> theory
   44.11    val add_judgment_cmd: binding * string * mixfix -> theory -> theory
   44.12 -  val judgment_name: theory -> string
   44.13 -  val is_judgment: theory -> term -> bool
   44.14 -  val drop_judgment: theory -> term -> term
   44.15 -  val fixed_judgment: theory -> string -> term
   44.16 -  val ensure_propT: theory -> term -> term
   44.17 -  val dest_judgment: cterm -> cterm
   44.18 -  val judgment_conv: conv -> conv
   44.19 -  val elim_concl: thm -> term option
   44.20 +  val judgment_name: Proof.context -> string
   44.21 +  val is_judgment: Proof.context -> term -> bool
   44.22 +  val drop_judgment: Proof.context -> term -> term
   44.23 +  val fixed_judgment: Proof.context -> string -> term
   44.24 +  val ensure_propT: Proof.context -> term -> term
   44.25 +  val dest_judgment: Proof.context -> cterm -> cterm
   44.26 +  val judgment_conv: Proof.context -> conv -> conv
   44.27 +  val elim_concl: Proof.context -> thm -> term option
   44.28    val declare_atomize: attribute
   44.29    val declare_rulify: attribute
   44.30 -  val atomize_term: theory -> term -> term
   44.31 +  val atomize_term: Proof.context -> term -> term
   44.32    val atomize: Proof.context -> conv
   44.33    val atomize_prems: Proof.context -> conv
   44.34    val atomize_prems_tac: Proof.context -> int -> tactic
   44.35    val full_atomize_tac: Proof.context -> int -> tactic
   44.36 -  val rulify_term: theory -> term -> term
   44.37 +  val rulify_term: Proof.context -> term -> term
   44.38    val rulify_tac: Proof.context -> int -> tactic
   44.39    val rulify: Proof.context -> thm -> thm
   44.40    val rulify_no_asm: Proof.context -> thm -> thm
   44.41 @@ -36,7 +36,7 @@
   44.42  structure Object_Logic: OBJECT_LOGIC =
   44.43  struct
   44.44  
   44.45 -(** theory data **)
   44.46 +(** context data **)
   44.47  
   44.48  datatype data = Data of
   44.49   {base_sort: sort option,
   44.50 @@ -46,7 +46,7 @@
   44.51  fun make_data (base_sort, judgment, atomize_rulify) =
   44.52    Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify};
   44.53  
   44.54 -structure Data = Theory_Data
   44.55 +structure Data = Generic_Data
   44.56  (
   44.57    type T = data;
   44.58    val empty = make_data (NONE, NONE, ([], []));
   44.59 @@ -66,7 +66,7 @@
   44.60  fun map_data f = Data.map (fn (Data {base_sort, judgment, atomize_rulify}) =>
   44.61    make_data (f (base_sort, judgment, atomize_rulify)));
   44.62  
   44.63 -fun get_data thy = Data.get thy |> (fn Data args => args);
   44.64 +fun get_data ctxt = Data.get (Context.Proof ctxt) |> (fn Data args => args);
   44.65  
   44.66  
   44.67  
   44.68 @@ -76,9 +76,10 @@
   44.69  
   44.70  val get_base_sort = #base_sort o get_data;
   44.71  
   44.72 -fun add_base_sort S = map_data (fn (base_sort, judgment, atomize_rulify) =>
   44.73 -  if is_some base_sort then error "Attempt to redeclare object-logic base sort"
   44.74 -  else (SOME S, judgment, atomize_rulify));
   44.75 +fun add_base_sort S =
   44.76 +  (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) =>
   44.77 +    if is_some base_sort then error "Attempt to redeclare object-logic base sort"
   44.78 +    else (SOME S, judgment, atomize_rulify));
   44.79  
   44.80  
   44.81  (* add judgment *)
   44.82 @@ -90,7 +91,7 @@
   44.83      thy
   44.84      |> add_consts [(b, T, mx)]
   44.85      |> (fn thy' => Theory.add_deps_global c (c, Sign.the_const_type thy' c) [] thy')
   44.86 -    |> map_data (fn (base_sort, judgment, atomize_rulify) =>
   44.87 +    |> (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) =>
   44.88          if is_some judgment then error "Attempt to redeclare object-logic judgment"
   44.89          else (base_sort, SOME c, atomize_rulify))
   44.90    end;
   44.91 @@ -105,51 +106,50 @@
   44.92  
   44.93  (* judgments *)
   44.94  
   44.95 -fun judgment_name thy =
   44.96 -  (case #judgment (get_data thy) of
   44.97 +fun judgment_name ctxt =
   44.98 +  (case #judgment (get_data ctxt) of
   44.99      SOME name => name
  44.100    | _ => raise TERM ("Unknown object-logic judgment", []));
  44.101  
  44.102 -fun is_judgment thy (Const (c, _) $ _) = c = judgment_name thy
  44.103 +fun is_judgment ctxt (Const (c, _) $ _) = c = judgment_name ctxt
  44.104    | is_judgment _ _ = false;
  44.105  
  44.106 -fun drop_judgment thy (Abs (x, T, t)) = Abs (x, T, drop_judgment thy t)
  44.107 -  | drop_judgment thy (tm as (Const (c, _) $ t)) =
  44.108 -      if (c = judgment_name thy handle TERM _ => false) then t else tm
  44.109 +fun drop_judgment ctxt (Abs (x, T, t)) = Abs (x, T, drop_judgment ctxt t)
  44.110 +  | drop_judgment ctxt (tm as (Const (c, _) $ t)) =
  44.111 +      if (c = judgment_name ctxt handle TERM _ => false) then t else tm
  44.112    | drop_judgment _ tm = tm;
  44.113  
  44.114 -fun fixed_judgment thy x =
  44.115 +fun fixed_judgment ctxt x =
  44.116    let  (*be robust wrt. low-level errors*)
  44.117 -    val c = judgment_name thy;
  44.118 +    val c = judgment_name ctxt;
  44.119      val aT = TFree (Name.aT, []);
  44.120      val T =
  44.121 -      the_default (aT --> propT) (Sign.const_type thy c)
  44.122 +      the_default (aT --> propT) (Sign.const_type (Proof_Context.theory_of ctxt) c)
  44.123        |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
  44.124      val U = Term.domain_type T handle Match => aT;
  44.125    in Const (c, T) $ Free (x, U) end;
  44.126  
  44.127 -fun ensure_propT thy t =
  44.128 +fun ensure_propT ctxt t =
  44.129    let val T = Term.fastype_of t
  44.130 -  in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end;
  44.131 +  in if T = propT then t else Const (judgment_name ctxt, T --> propT) $ t end;
  44.132  
  44.133 -fun dest_judgment ct =
  44.134 -  if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct)
  44.135 +fun dest_judgment ctxt ct =
  44.136 +  if is_judgment ctxt (Thm.term_of ct)
  44.137    then Thm.dest_arg ct
  44.138    else raise CTERM ("dest_judgment", [ct]);
  44.139  
  44.140 -fun judgment_conv cv ct =
  44.141 -  if is_judgment (Thm.theory_of_cterm ct) (Thm.term_of ct)
  44.142 +fun judgment_conv ctxt cv ct =
  44.143 +  if is_judgment ctxt (Thm.term_of ct)
  44.144    then Conv.arg_conv cv ct
  44.145    else raise CTERM ("judgment_conv", [ct]);
  44.146  
  44.147  
  44.148  (* elimination rules *)
  44.149  
  44.150 -fun elim_concl rule =
  44.151 +fun elim_concl ctxt rule =
  44.152    let
  44.153 -    val thy = Thm.theory_of_thm rule;
  44.154      val concl = Thm.concl_of rule;
  44.155 -    val C = drop_judgment thy concl;
  44.156 +    val C = drop_judgment ctxt concl;
  44.157    in
  44.158      if Term.is_Var C andalso
  44.159        exists (fn prem => concl aconv Logic.strip_assums_concl prem) (Thm.prems_of rule)
  44.160 @@ -171,19 +171,19 @@
  44.161  fun add_rulify th = map_data (fn (base_sort, judgment, (atomize, rulify)) =>
  44.162    (base_sort, judgment, (atomize, Thm.add_thm th rulify)));
  44.163  
  44.164 -val declare_atomize = Thm.declaration_attribute (fn th => Context.mapping (add_atomize th) I);
  44.165 -val declare_rulify = Thm.declaration_attribute (fn th => Context.mapping (add_rulify th) I);
  44.166 +val declare_atomize = Thm.declaration_attribute add_atomize;
  44.167 +val declare_rulify = Thm.declaration_attribute add_rulify;
  44.168  
  44.169 -val _ = Theory.setup (fold add_rulify Drule.norm_hhf_eqs);
  44.170 +val _ = Theory.setup (fold (Context.theory_map o add_rulify) Drule.norm_hhf_eqs);
  44.171  
  44.172  
  44.173  (* atomize *)
  44.174  
  44.175 -fun atomize_term thy =
  44.176 -  drop_judgment thy o Raw_Simplifier.rewrite_term thy (get_atomize thy) [];
  44.177 +fun atomize_term ctxt =
  44.178 +  drop_judgment ctxt o
  44.179 +    Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) (get_atomize ctxt) [];
  44.180  
  44.181 -fun atomize ctxt =
  44.182 -  Raw_Simplifier.rewrite ctxt true (get_atomize (Proof_Context.theory_of ctxt));
  44.183 +fun atomize ctxt = Raw_Simplifier.rewrite ctxt true (get_atomize ctxt);
  44.184  
  44.185  fun atomize_prems ctxt ct =
  44.186    if Logic.has_meta_prems (Thm.term_of ct) then
  44.187 @@ -196,11 +196,13 @@
  44.188  
  44.189  (* rulify *)
  44.190  
  44.191 -fun rulify_term thy = Raw_Simplifier.rewrite_term thy (get_rulify thy) [];
  44.192 -fun rulify_tac ctxt = rewrite_goal_tac ctxt (get_rulify (Proof_Context.theory_of ctxt));
  44.193 +fun rulify_term ctxt =
  44.194 +  Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) (get_rulify ctxt) [];
  44.195 +
  44.196 +fun rulify_tac ctxt = rewrite_goal_tac ctxt (get_rulify ctxt);
  44.197  
  44.198  fun gen_rulify full ctxt =
  44.199 -  Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify (Proof_Context.theory_of ctxt)))
  44.200 +  Conv.fconv_rule (Raw_Simplifier.rewrite ctxt full (get_rulify ctxt))
  44.201    #> Drule.gen_all (Variable.maxidx_of ctxt)
  44.202    #> Thm.strip_shyps
  44.203    #> Drule.zero_var_indexes;
    45.1 --- a/src/Pure/Isar/obtain.ML	Wed Apr 08 19:24:32 2015 +0200
    45.2 +++ b/src/Pure/Isar/obtain.ML	Wed Apr 08 22:15:03 2015 +0200
    45.3 @@ -73,10 +73,8 @@
    45.4  
    45.5  fun eliminate fix_ctxt rule xs As thm =
    45.6    let
    45.7 -    val thy = Proof_Context.theory_of fix_ctxt;
    45.8 -
    45.9      val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm);
   45.10 -    val _ = Object_Logic.is_judgment thy (Thm.concl_of thm) orelse
   45.11 +    val _ = Object_Logic.is_judgment fix_ctxt (Thm.concl_of thm) orelse
   45.12        error "Conclusion in obtained context must be object-logic judgment";
   45.13  
   45.14      val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt;
   45.15 @@ -99,9 +97,8 @@
   45.16  
   45.17  fun bind_judgment ctxt name =
   45.18    let
   45.19 -    val thy = Proof_Context.theory_of ctxt;
   45.20      val ([x], ctxt') = Proof_Context.add_fixes [(Binding.name name, NONE, NoSyn)] ctxt;
   45.21 -    val (t as _ $ Free v) = Object_Logic.fixed_judgment thy x;
   45.22 +    val (t as _ $ Free v) = Object_Logic.fixed_judgment ctxt x;
   45.23    in ((v, t), ctxt') end;
   45.24  
   45.25  val thatN = "that";
    46.1 --- a/src/Pure/Isar/proof.ML	Wed Apr 08 19:24:32 2015 +0200
    46.2 +++ b/src/Pure/Isar/proof.ML	Wed Apr 08 22:15:03 2015 +0200
    46.3 @@ -406,9 +406,8 @@
    46.4  
    46.5  fun no_goal_cases st = map (rpair NONE) (goals st);
    46.6  
    46.7 -fun goal_cases st =
    46.8 -  Rule_Cases.make_common
    46.9 -    (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
   46.10 +fun goal_cases ctxt st =
   46.11 +  Rule_Cases.make_common ctxt (Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
   46.12  
   46.13  fun apply_method text ctxt state =
   46.14    #2 (#2 (find_goal state)) |> (fn {statement, using, goal, before_qed, after_qed} =>
   46.15 @@ -416,7 +415,7 @@
   46.16      |> Seq.map (fn (meth_cases, goal') =>
   46.17        state
   46.18        |> map_goal
   46.19 -          (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #>
   46.20 +          (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases ctxt goal') #>
   46.21             Proof_Context.update_cases true meth_cases)
   46.22            (K (statement, using, goal', before_qed, after_qed)) I));
   46.23  
    47.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 08 19:24:32 2015 +0200
    47.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 08 22:15:03 2015 +0200
    47.3 @@ -842,7 +842,7 @@
    47.4  fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
    47.5    | drop_schematic b = b;
    47.6  
    47.7 -fun auto_bind f ts ctxt = ctxt |> bind_terms (map drop_schematic (f (theory_of ctxt) ts));
    47.8 +fun auto_bind f ts ctxt = ctxt |> bind_terms (map drop_schematic (f ctxt ts));
    47.9  
   47.10  val auto_bind_goal = auto_bind Auto_Bind.goal;
   47.11  val auto_bind_facts = auto_bind Auto_Bind.facts;
    48.1 --- a/src/Pure/Isar/rule_cases.ML	Wed Apr 08 19:24:32 2015 +0200
    48.2 +++ b/src/Pure/Isar/rule_cases.ML	Wed Apr 08 22:15:03 2015 +0200
    48.3 @@ -13,7 +13,7 @@
    48.4    type cases_tactic = thm -> cases_state Seq.seq
    48.5    val CASES: cases -> tactic -> cases_tactic
    48.6    val EMPTY_CASES: tactic -> cases_tactic
    48.7 -  val SUBGOAL_CASES: ((term * int * thm) -> cases_tactic) -> int -> cases_tactic
    48.8 +  val SUBGOAL_CASES: (term * int -> cases_tactic) -> int -> cases_tactic
    48.9    val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
   48.10  end
   48.11  
   48.12 @@ -27,9 +27,9 @@
   48.13      cases: (string * T) list}
   48.14    val case_hypsN: string
   48.15    val strip_params: term -> (string * typ) list
   48.16 -  val make_common: theory * term ->
   48.17 +  val make_common: Proof.context -> term ->
   48.18      ((string * string list) * string list) list -> cases
   48.19 -  val make_nested: term -> theory * term ->
   48.20 +  val make_nested: Proof.context -> term -> term ->
   48.21      ((string * string list) * string list) list -> cases
   48.22    val apply: term list -> T -> T
   48.23    val consume: Proof.context -> thm list -> thm list -> ('a * int) * thm ->
   48.24 @@ -107,9 +107,9 @@
   48.25  
   48.26  fun bindings args = map (apfst Binding.name) args;
   48.27  
   48.28 -fun extract_case thy (case_outline, raw_prop) name hyp_names concls =
   48.29 +fun extract_case ctxt (case_outline, raw_prop) name hyp_names concls =
   48.30    let
   48.31 -    val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
   48.32 +    val props = Logic.dest_conjunctions (Drule.norm_hhf (Proof_Context.theory_of ctxt) raw_prop);
   48.33      val len = length props;
   48.34      val nested = is_some case_outline andalso len > 1;
   48.35  
   48.36 @@ -126,7 +126,7 @@
   48.37            extract_assumes name hyp_names case_outline prop
   48.38            |> apply2 (map (apsnd (maps Logic.dest_conjunctions)));
   48.39  
   48.40 -        val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
   48.41 +        val concl = Object_Logic.drop_judgment ctxt (Logic.strip_assums_concl prop);
   48.42          val binds =
   48.43            (case_conclN, concl) :: dest_binops concls concl
   48.44            |> map (fn (x, t) => ((x, 0), SOME (abs_fixes t)));
   48.45 @@ -152,7 +152,7 @@
   48.46      else SOME (nested_case (hd cases))
   48.47    end;
   48.48  
   48.49 -fun make rule_struct (thy, prop) cases =
   48.50 +fun make ctxt rule_struct prop cases =
   48.51    let
   48.52      val n = length cases;
   48.53      val nprems = Logic.count_prems prop;
   48.54 @@ -160,13 +160,13 @@
   48.55        ((case try (fn () =>
   48.56            (Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
   48.57          NONE => (name, NONE)
   48.58 -      | SOME p => (name, extract_case thy p name hyp_names concls)) :: cs, i - 1);
   48.59 +      | SOME p => (name, extract_case ctxt p name hyp_names concls)) :: cs, i - 1);
   48.60    in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end;
   48.61  
   48.62  in
   48.63  
   48.64 -val make_common = make NONE;
   48.65 -fun make_nested rule_struct = make (SOME rule_struct);
   48.66 +fun make_common ctxt = make ctxt NONE;
   48.67 +fun make_nested ctxt rule_struct = make ctxt (SOME rule_struct);
   48.68  
   48.69  fun apply args =
   48.70    let
   48.71 @@ -192,7 +192,7 @@
   48.72  
   48.73  fun SUBGOAL_CASES tac i st =
   48.74    (case try Logic.nth_prem (i, Thm.prop_of st) of
   48.75 -    SOME goal => tac (goal, i, st) st
   48.76 +    SOME goal => tac (goal, i) st
   48.77    | NONE => Seq.empty);
   48.78  
   48.79  fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
    49.1 --- a/src/Pure/Isar/specification.ML	Wed Apr 08 19:24:32 2015 +0200
    49.2 +++ b/src/Pure/Isar/specification.ML	Wed Apr 08 22:15:03 2015 +0200
    49.3 @@ -356,7 +356,7 @@
    49.4          val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
    49.5          val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
    49.6  
    49.7 -        val thesis = Object_Logic.fixed_judgment (Proof_Context.theory_of ctxt) Auto_Bind.thesisN;
    49.8 +        val thesis = Object_Logic.fixed_judgment ctxt Auto_Bind.thesisN;
    49.9  
   49.10          fun assume_case ((name, (vars, _)), asms) ctxt' =
   49.11            let
    50.1 --- a/src/Pure/Isar/typedecl.ML	Wed Apr 08 19:24:32 2015 +0200
    50.2 +++ b/src/Pure/Isar/typedecl.ML	Wed Apr 08 22:15:03 2015 +0200
    50.3 @@ -26,11 +26,6 @@
    50.4  
    50.5  (* primitives *)
    50.6  
    50.7 -fun object_logic_arity name thy =
    50.8 -  (case Object_Logic.get_base_sort thy of
    50.9 -    NONE => thy
   50.10 -  | SOME S => Axclass.arity_axiomatization (name, replicate (Sign.arity_number thy name) S, S) thy);
   50.11 -
   50.12  fun basic_decl decl (b, n, mx) lthy =
   50.13    let val name = Local_Theory.full_name lthy b in
   50.14      lthy
   50.15 @@ -41,8 +36,11 @@
   50.16    end;
   50.17  
   50.18  fun basic_typedecl (b, n, mx) lthy =
   50.19 -  basic_decl (fn name => Sign.add_type lthy (b, n, NoSyn) #> object_logic_arity name)
   50.20 -    (b, n, mx) lthy;
   50.21 +  basic_decl (fn name =>
   50.22 +    Sign.add_type lthy (b, n, NoSyn) #>
   50.23 +    (case Object_Logic.get_base_sort lthy of
   50.24 +      SOME S => Axclass.arity_axiomatization (name, replicate n S, S)
   50.25 +    | NONE => I)) (b, n, mx) lthy;
   50.26  
   50.27  
   50.28  (* global type -- without dependencies on type parameters of the context *)
    51.1 --- a/src/Pure/Thy/term_style.ML	Wed Apr 08 19:24:32 2015 +0200
    51.2 +++ b/src/Pure/Thy/term_style.ML	Wed Apr 08 22:15:03 2015 +0200
    51.3 @@ -49,8 +49,7 @@
    51.4  
    51.5  fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
    51.6    let
    51.7 -    val concl =
    51.8 -      Object_Logic.drop_judgment (Proof_Context.theory_of ctxt) (Logic.strip_imp_concl t)
    51.9 +    val concl = Object_Logic.drop_judgment ctxt (Logic.strip_imp_concl t);
   51.10    in
   51.11      (case concl of
   51.12        _ $ l $ r => proj (l, r)
    52.1 --- a/src/Pure/Tools/find_theorems.ML	Wed Apr 08 19:24:32 2015 +0200
    52.2 +++ b/src/Pure/Tools/find_theorems.ML	Wed Apr 08 22:15:03 2015 +0200
    52.3 @@ -89,7 +89,7 @@
    52.4  
    52.5  (* matching theorems *)
    52.6  
    52.7 -fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
    52.8 +fun is_nontrivial ctxt = Term.is_Const o Term.head_of o Object_Logic.drop_judgment ctxt;
    52.9  
   52.10  (*extract terms from term_src, refine them to the parts that concern us,
   52.11    if po try match them against obj else vice versa.
   52.12 @@ -100,7 +100,7 @@
   52.13      val thy = Proof_Context.theory_of ctxt;
   52.14  
   52.15      fun matches pat =
   52.16 -      is_nontrivial thy pat andalso
   52.17 +      is_nontrivial ctxt pat andalso
   52.18        Pattern.matches thy (if po then (pat, obj) else (obj, pat));
   52.19  
   52.20      fun subst_size pat =
   52.21 @@ -171,8 +171,7 @@
   52.22      in
   52.23        (*elim rules always have assumptions, so an elim with one
   52.24          assumption is as good as an intro rule with none*)
   52.25 -      if is_nontrivial (Proof_Context.theory_of ctxt) (Thm.major_prem_of thm)
   52.26 -          andalso not (null successful) then
   52.27 +      if is_nontrivial ctxt (Thm.major_prem_of thm) andalso not (null successful) then
   52.28          SOME (size_of_term (Thm.prop_of thm), Thm.nprems_of thm - 1, foldl1 Int.min successful)
   52.29        else NONE
   52.30      end
    53.1 --- a/src/Pure/more_thm.ML	Wed Apr 08 19:24:32 2015 +0200
    53.2 +++ b/src/Pure/more_thm.ML	Wed Apr 08 22:15:03 2015 +0200
    53.3 @@ -68,6 +68,8 @@
    53.4    val forall_intr_frees: thm -> thm
    53.5    val unvarify_global: thm -> thm
    53.6    val close_derivation: thm -> thm
    53.7 +  val rename_params_rule: string list * int -> thm -> thm
    53.8 +  val rename_boundvars: term -> term -> thm -> thm
    53.9    val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory
   53.10    val add_axiom_global: binding * term -> theory -> (string * thm) * theory
   53.11    val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory
   53.12 @@ -392,6 +394,38 @@
   53.13    else thm;
   53.14  
   53.15  
   53.16 +(* user renaming of parameters in a subgoal *)
   53.17 +
   53.18 +(*The names, if distinct, are used for the innermost parameters of subgoal i;
   53.19 +  preceding parameters may be renamed to make all parameters distinct.*)
   53.20 +fun rename_params_rule (names, i) st =
   53.21 +  let
   53.22 +    val (_, Bs, Bi, C) = Thm.dest_state (st, i);
   53.23 +    val params = map #1 (Logic.strip_params Bi);
   53.24 +    val short = length params - length names;
   53.25 +    val names' =
   53.26 +      if short < 0 then error "More names than parameters in subgoal!"
   53.27 +      else Name.variant_list names (take short params) @ names;
   53.28 +    val free_names = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
   53.29 +    val Bi' = Logic.list_rename_params names' Bi;
   53.30 +  in
   53.31 +    (case duplicates (op =) names of
   53.32 +      a :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ a); st)
   53.33 +    | [] =>
   53.34 +      (case inter (op =) names free_names of
   53.35 +        a :: _ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); st)
   53.36 +      | [] => Thm.renamed_prop (Logic.list_implies (Bs @ [Bi'], C)) st))
   53.37 +  end;
   53.38 +
   53.39 +
   53.40 +(* preservation of bound variable names *)
   53.41 +
   53.42 +fun rename_boundvars pat obj th =
   53.43 +  (case Term.rename_abs pat obj (Thm.prop_of th) of
   53.44 +    NONE => th
   53.45 +  | SOME prop' => Thm.renamed_prop prop' th);
   53.46 +
   53.47 +
   53.48  
   53.49  (** specification primitives **)
   53.50  
    54.1 --- a/src/Pure/thm.ML	Wed Apr 08 19:24:32 2015 +0200
    54.2 +++ b/src/Pure/thm.ML	Wed Apr 08 22:15:03 2015 +0200
    54.3 @@ -34,6 +34,7 @@
    54.4    val maxidx_of_cterm: cterm -> int
    54.5    val global_cterm_of: theory -> term -> cterm
    54.6    val cterm_of: Proof.context -> term -> cterm
    54.7 +  val renamed_term: term -> cterm -> cterm
    54.8    val dest_comb: cterm -> cterm * cterm
    54.9    val dest_fun: cterm -> cterm
   54.10    val dest_arg: cterm -> cterm
   54.11 @@ -81,6 +82,7 @@
   54.12    val cprop_of: thm -> cterm
   54.13    val cprem_of: thm -> int -> cterm
   54.14    val transfer: theory -> thm -> thm
   54.15 +  val renamed_prop: term -> thm -> thm
   54.16    val weaken: cterm -> thm -> thm
   54.17    val weaken_sorts: sort list -> cterm -> cterm
   54.18    val extra_shyps: thm -> sort list
   54.19 @@ -125,14 +127,13 @@
   54.20    val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
   54.21    val varifyT_global: thm -> thm
   54.22    val legacy_freezeT: thm -> thm
   54.23 +  val dest_state: thm * int -> (term * term) list * term list * term * term
   54.24    val lift_rule: cterm -> thm -> thm
   54.25    val incr_indexes: int -> thm -> thm
   54.26    val assumption: Proof.context option -> int -> thm -> thm Seq.seq
   54.27    val eq_assumption: int -> thm -> thm
   54.28    val rotate_rule: int -> int -> thm -> thm
   54.29    val permute_prems: int -> int -> thm -> thm
   54.30 -  val rename_params_rule: string list * int -> thm -> thm
   54.31 -  val rename_boundvars: term -> term -> thm -> thm
   54.32    val bicompose: Proof.context option -> {flatten: bool, match: bool, incremented: bool} ->
   54.33      bool * thm * int -> int -> thm -> thm Seq.seq
   54.34    val biresolution: Proof.context option -> bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
   54.35 @@ -195,6 +196,10 @@
   54.36  
   54.37  val cterm_of = global_cterm_of o Proof_Context.theory_of;
   54.38  
   54.39 +fun renamed_term t' (Cterm {thy, t, T, maxidx, sorts}) =
   54.40 +  if t aconv t' then Cterm {thy = thy, t = t', T = T, maxidx = maxidx, sorts = sorts}
   54.41 +  else raise TERM ("renamed_term: terms disagree", [t, t']);
   54.42 +
   54.43  fun merge_thys0 (Cterm {thy = thy1, ...}) (Cterm {thy = thy2, ...}) =
   54.44    Theory.merge (thy1, thy2);
   54.45  
   54.46 @@ -416,6 +421,13 @@
   54.47          prop = prop})
   54.48    end;
   54.49  
   54.50 +(*implicit alpha-conversion*)
   54.51 +fun renamed_prop prop' (Thm (der, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) =
   54.52 +  if prop aconv prop' then
   54.53 +    Thm (der, {thy = thy, tags = tags, maxidx = maxidx, shyps = shyps,
   54.54 +      hyps = hyps, tpairs = tpairs, prop = prop'})
   54.55 +  else raise TERM ("renamed_prop: props disagree", [prop, prop']);
   54.56 +
   54.57  fun make_context NONE thy = Context.Theory thy
   54.58    | make_context (SOME ctxt) thy =
   54.59        if Theory.subthy (thy, Proof_Context.theory_of ctxt) then Context.Proof ctxt
   54.60 @@ -1426,56 +1438,6 @@
   54.61    end;
   54.62  
   54.63  
   54.64 -(** User renaming of parameters in a subgoal **)
   54.65 -
   54.66 -(*Calls error rather than raising an exception because it is intended
   54.67 -  for top-level use -- exception handling would not make sense here.
   54.68 -  The names in cs, if distinct, are used for the innermost parameters;
   54.69 -  preceding parameters may be renamed to make all params distinct.*)
   54.70 -fun rename_params_rule (cs, i) state =
   54.71 -  let
   54.72 -    val Thm (der, {thy, tags, maxidx, shyps, hyps, ...}) = state;
   54.73 -    val (tpairs, Bs, Bi, C) = dest_state (state, i);
   54.74 -    val iparams = map #1 (Logic.strip_params Bi);
   54.75 -    val short = length iparams - length cs;
   54.76 -    val newnames =
   54.77 -      if short < 0 then error "More names than abstractions!"
   54.78 -      else Name.variant_list cs (take short iparams) @ cs;
   54.79 -    val freenames = Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) Bi [];
   54.80 -    val newBi = Logic.list_rename_params newnames Bi;
   54.81 -  in
   54.82 -    (case duplicates (op =) cs of
   54.83 -      a :: _ => (warning ("Can't rename.  Bound variables not distinct: " ^ a); state)
   54.84 -    | [] =>
   54.85 -      (case inter (op =) cs freenames of
   54.86 -        a :: _ => (warning ("Can't rename.  Bound/Free variable clash: " ^ a); state)
   54.87 -      | [] =>
   54.88 -        Thm (der,
   54.89 -         {thy = thy,
   54.90 -          tags = tags,
   54.91 -          maxidx = maxidx,
   54.92 -          shyps = shyps,
   54.93 -          hyps = hyps,
   54.94 -          tpairs = tpairs,
   54.95 -          prop = Logic.list_implies (Bs @ [newBi], C)})))
   54.96 -  end;
   54.97 -
   54.98 -
   54.99 -(*** Preservation of bound variable names ***)
  54.100 -
  54.101 -fun rename_boundvars pat obj (thm as Thm (der, {thy, tags, maxidx, shyps, hyps, tpairs, prop})) =
  54.102 -  (case Term.rename_abs pat obj prop of
  54.103 -    NONE => thm
  54.104 -  | SOME prop' => Thm (der,
  54.105 -      {thy = thy,
  54.106 -       tags = tags,
  54.107 -       maxidx = maxidx,
  54.108 -       hyps = hyps,
  54.109 -       shyps = shyps,
  54.110 -       tpairs = tpairs,
  54.111 -       prop = prop'}));
  54.112 -
  54.113 -
  54.114  (* strip_apply f B A strips off all assumptions/parameters from A
  54.115     introduced by lifting over B, and applies f to remaining part of A*)
  54.116  fun strip_apply f =
    55.1 --- a/src/Tools/atomize_elim.ML	Wed Apr 08 19:24:32 2015 +0200
    55.2 +++ b/src/Tools/atomize_elim.ML	Wed Apr 08 22:15:03 2015 +0200
    55.3 @@ -55,7 +55,7 @@
    55.4  fun atomize_elim_conv ctxt ct =
    55.5      (forall_conv (prems_conv ~1 o Object_Logic.atomize_prems o snd) ctxt
    55.6      then_conv Raw_Simplifier.rewrite ctxt true (Named_Theorems.get ctxt named_theorems)
    55.7 -    then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
    55.8 +    then_conv (fn ct' => if can (Object_Logic.dest_judgment ctxt) ct'
    55.9                           then all_conv ct'
   55.10                           else raise CTERM ("atomize_elim", [ct', ct])))
   55.11      ct
    56.1 --- a/src/Tools/induct.ML	Wed Apr 08 19:24:32 2015 +0200
    56.2 +++ b/src/Tools/induct.ML	Wed Apr 08 22:15:03 2015 +0200
    56.3 @@ -59,11 +59,11 @@
    56.4    val arbitrary_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
    56.5    val add_defs: (binding option * (term * bool)) option list -> Proof.context ->
    56.6      (term option list * thm list) * Proof.context
    56.7 -  val atomize_term: theory -> term -> term
    56.8 +  val atomize_term: Proof.context -> term -> term
    56.9    val atomize_cterm: Proof.context -> conv
   56.10    val atomize_tac: Proof.context -> int -> tactic
   56.11    val inner_atomize_tac: Proof.context -> int -> tactic
   56.12 -  val rulified_term: thm -> theory * term
   56.13 +  val rulified_term: Proof.context -> thm -> term
   56.14    val rulify_tac: Proof.context -> int -> tactic
   56.15    val simplified_rule: Proof.context -> thm -> thm
   56.16    val simplify_tac: Proof.context -> int -> tactic
   56.17 @@ -75,7 +75,7 @@
   56.18      thm list -> int -> cases_tactic
   56.19    val get_inductT: Proof.context -> term option list list -> thm list list
   56.20    type case_data = (((string * string list) * string list) list * int) (* FIXME -> rule_cases.ML *)
   56.21 -  val gen_induct_tac: (theory -> case_data * thm -> case_data * thm) ->
   56.22 +  val gen_induct_tac: (case_data * thm -> case_data * thm) ->
   56.23      Proof.context -> bool -> (binding option * (term * bool)) option list list ->
   56.24      (string * typ) list list -> term option list -> thm list option ->
   56.25      thm list -> int -> cases_tactic
   56.26 @@ -137,14 +137,12 @@
   56.27        Conv.implies_concl_conv (swap_prems_conv (i - 1)) then_conv
   56.28        Conv.rewr_conv Drule.swap_prems_eq
   56.29  
   56.30 -fun drop_judgment ctxt = Object_Logic.drop_judgment (Proof_Context.theory_of ctxt);
   56.31 -
   56.32  fun find_eq ctxt t =
   56.33    let
   56.34      val l = length (Logic.strip_params t);
   56.35      val Hs = Logic.strip_assums_hyp t;
   56.36      fun find (i, t) =
   56.37 -      (case Induct_Args.dest_def (drop_judgment ctxt t) of
   56.38 +      (case Induct_Args.dest_def (Object_Logic.drop_judgment ctxt t) of
   56.39          SOME (Bound j, _) => SOME (i, j)
   56.40        | SOME (_, Bound j) => SOME (i, j)
   56.41        | _ => NONE);
   56.42 @@ -167,11 +165,11 @@
   56.43  
   56.44  (* rotate k premises to the left by j, skipping over first j premises *)
   56.45  
   56.46 -fun rotate_conv 0 j 0 = Conv.all_conv
   56.47 +fun rotate_conv 0 _ 0 = Conv.all_conv
   56.48    | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k - 1)
   56.49    | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i - 1) j k);
   56.50  
   56.51 -fun rotate_tac j 0 = K all_tac
   56.52 +fun rotate_tac _ 0 = K all_tac
   56.53    | rotate_tac j k = SUBGOAL (fn (goal, i) =>
   56.54        CONVERSION (rotate_conv
   56.55          j (length (Logic.strip_assums_hyp goal) - j - k) k) i);
   56.56 @@ -181,7 +179,7 @@
   56.57  
   56.58  fun rulify_defs_conv ctxt ct =
   56.59    if exists_subterm (is_some o Induct_Args.dest_def) (Thm.term_of ct) andalso
   56.60 -    not (is_some (Induct_Args.dest_def (drop_judgment ctxt (Thm.term_of ct))))
   56.61 +    not (is_some (Induct_Args.dest_def (Object_Logic.drop_judgment ctxt (Thm.term_of ct))))
   56.62    then
   56.63      (Conv.forall_conv (rulify_defs_conv o snd) ctxt else_conv
   56.64       Conv.implies_conv (Conv.try_conv (rulify_defs_conv ctxt))
   56.65 @@ -502,8 +500,8 @@
   56.66            val rule' = rule
   56.67              |> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt);
   56.68          in
   56.69 -          CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt,
   56.70 -              Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
   56.71 +          CASES (Rule_Cases.make_common ctxt
   56.72 +              (Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
   56.73              ((Method.insert_tac more_facts THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
   56.74                  (if simp then TRY o trivial_tac ctxt else K all_tac)) i) st
   56.75          end)
   56.76 @@ -520,9 +518,9 @@
   56.77  
   56.78  (* atomize *)
   56.79  
   56.80 -fun atomize_term thy =
   56.81 -  Raw_Simplifier.rewrite_term thy Induct_Args.atomize []
   56.82 -  #> Object_Logic.drop_judgment thy;
   56.83 +fun atomize_term ctxt =
   56.84 +  Raw_Simplifier.rewrite_term (Proof_Context.theory_of ctxt) Induct_Args.atomize []
   56.85 +  #> Object_Logic.drop_judgment ctxt;
   56.86  
   56.87  fun atomize_cterm ctxt = Raw_Simplifier.rewrite ctxt true Induct_Args.atomize;
   56.88  
   56.89 @@ -538,12 +536,11 @@
   56.90    Raw_Simplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #>
   56.91    Raw_Simplifier.rewrite_term thy Induct_Args.rulify_fallback [];
   56.92  
   56.93 -fun rulified_term thm =
   56.94 +fun rulified_term ctxt thm =
   56.95    let
   56.96 -    val thy = Thm.theory_of_thm thm;
   56.97 -    val rulify = rulify_term thy;
   56.98 +    val rulify = rulify_term (Proof_Context.theory_of ctxt);
   56.99      val (As, B) = Logic.strip_horn (Thm.prop_of thm);
  56.100 -  in (thy, Logic.list_implies (map rulify As, rulify B)) end;
  56.101 +  in Logic.list_implies (map rulify As, rulify B) end;
  56.102  
  56.103  fun rulify_tac ctxt =
  56.104    rewrite_goal_tac ctxt (Induct_Args.rulify @ conjunction_congs) THEN'
  56.105 @@ -606,7 +603,7 @@
  56.106  fun special_rename_params ctxt [[SOME (Free (z, Type (T, _)))]] [thm] =
  56.107        let
  56.108          val x = Name.clean (Variable.revert_fixed ctxt z);
  56.109 -        fun index i [] = []
  56.110 +        fun index _ [] = []
  56.111            | index i (y :: ys) =
  56.112                if x = y then x ^ string_of_int i :: index (i + 1) ys
  56.113                else y :: index i ys;
  56.114 @@ -734,10 +731,8 @@
  56.115  type case_data = (((string * string list) * string list) list * int);
  56.116  
  56.117  fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
  56.118 -  SUBGOAL_CASES (fn (_, i, st) =>
  56.119 +  SUBGOAL_CASES (fn (_, i) =>
  56.120      let
  56.121 -      val thy = Proof_Context.theory_of ctxt;
  56.122 -
  56.123        val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
  56.124        val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
  56.125  
  56.126 @@ -745,9 +740,9 @@
  56.127          (if null insts then `Rule_Cases.get r
  56.128           else (align_left "Rule has fewer conclusions than arguments given"
  56.129              (map Logic.strip_imp_concl (Logic.dest_conjunctions (Thm.concl_of r))) insts
  56.130 -          |> maps (prep_inst ctxt align_right (atomize_term thy))
  56.131 +          |> maps (prep_inst ctxt align_right (atomize_term ctxt))
  56.132            |> Drule.cterm_instantiate) r |> pair (Rule_Cases.get r))
  56.133 -        |> mod_cases thy
  56.134 +        |> mod_cases
  56.135          |> (fn ((cases, consumes), th) => (((cases, concls), consumes), th));
  56.136  
  56.137        val ruleq =
  56.138 @@ -766,7 +761,7 @@
  56.139            val rule'' = rule' |> simp ? simplified_rule ctxt;
  56.140            val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
  56.141            val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
  56.142 -        in Rule_Cases.make_nested (Thm.prop_of rule'') (rulified_term rule'') cases' end;
  56.143 +        in Rule_Cases.make_nested ctxt (Thm.prop_of rule'') (rulified_term ctxt rule'') cases' end;
  56.144      in
  56.145        fn st =>
  56.146          ruleq
  56.147 @@ -800,7 +795,7 @@
  56.148          ((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac ctxt) else K all_tac)
  56.149           THEN_ALL_NEW rulify_tac ctxt);
  56.150  
  56.151 -val induct_tac = gen_induct_tac (K I);
  56.152 +val induct_tac = gen_induct_tac I;
  56.153  
  56.154  
  56.155  
  56.156 @@ -825,30 +820,27 @@
  56.157  
  56.158  in
  56.159  
  56.160 -fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i, st) =>
  56.161 +fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i) =>
  56.162    let
  56.163      fun inst_rule r =
  56.164        if null inst then `Rule_Cases.get r
  56.165        else Drule.cterm_instantiate (prep_inst ctxt align_right I (main_prop_of r, inst)) r
  56.166          |> pair (Rule_Cases.get r);
  56.167 -
  56.168 -    fun ruleq goal =
  56.169 +  in
  56.170 +    fn st =>
  56.171        (case opt_rule of
  56.172          SOME r => Seq.single (inst_rule r)
  56.173        | NONE =>
  56.174            (get_coinductP ctxt goal @ get_coinductT ctxt inst)
  56.175            |> tap (trace_rules ctxt coinductN)
  56.176 -          |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
  56.177 -  in
  56.178 -    fn st =>
  56.179 -      ruleq goal
  56.180 +          |> Seq.of_list |> Seq.maps (Seq.try inst_rule))
  56.181        |> Seq.maps (Rule_Cases.consume ctxt [] facts)
  56.182        |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
  56.183          guess_instance ctxt rule i st
  56.184          |> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
  56.185          |> Seq.maps (fn rule' =>
  56.186 -          CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt,
  56.187 -              Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
  56.188 +          CASES (Rule_Cases.make_common ctxt
  56.189 +              (Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
  56.190              (Method.insert_tac more_facts i THEN resolve_tac ctxt [rule'] i) st))
  56.191    end);
  56.192  
    57.1 --- a/src/Tools/induction.ML	Wed Apr 08 19:24:32 2015 +0200
    57.2 +++ b/src/Tools/induction.ML	Wed Apr 08 22:15:03 2015 +0200
    57.3 @@ -43,7 +43,7 @@
    57.4            (take n cases ~~ take n hnamess);
    57.5      in ((cases', consumes), th) end;
    57.6  
    57.7 -val induction_tac = Induct.gen_induct_tac (K name_hyps);
    57.8 +val induction_tac = Induct.gen_induct_tac name_hyps;
    57.9  
   57.10  val _ = Theory.local_setup (Induct.gen_induct_setup @{binding induction} induction_tac);
   57.11