merged
authorwenzelm
Fri Oct 29 11:07:21 2010 +0200 (2010-10-29)
changeset 40253f99ec71de82d
parent 40252 029400b6c893
parent 40242 bb433b0668b8
child 40254 6d1ebaa7a4ba
child 40257 323f7aad54b0
merged
NEWS
src/FOL/ex/Iff_Oracle.thy
src/Tools/quickcheck.ML
     1.1 --- a/NEWS	Fri Oct 29 11:04:41 2010 +0200
     1.2 +++ b/NEWS	Fri Oct 29 11:07:21 2010 +0200
     1.3 @@ -344,6 +344,10 @@
     1.4  Fail if the argument is false.  Due to inlining the source position of
     1.5  failed assertions is included in the error output.
     1.6  
     1.7 +* Discontinued antiquotation @{theory_ref}, which is obsolete since ML
     1.8 +text is in practice always evaluated with a stable theory checkpoint.
     1.9 +Minor INCOMPATIBILITY, use (Theory.check_thy @{theory}) instead.
    1.10 +
    1.11  * Renamed setmp_noncritical to Unsynchronized.setmp to emphasize its
    1.12  meaning.
    1.13  
     2.1 --- a/doc-src/IsarImplementation/Thy/Prelim.thy	Fri Oct 29 11:04:41 2010 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Fri Oct 29 11:07:21 2010 +0200
     2.3 @@ -226,11 +226,10 @@
     2.4  text %mlantiq {*
     2.5    \begin{matharray}{rcl}
     2.6    @{ML_antiquotation_def "theory"} & : & @{text ML_antiquotation} \\
     2.7 -  @{ML_antiquotation_def "theory_ref"} & : & @{text ML_antiquotation} \\
     2.8    \end{matharray}
     2.9  
    2.10    \begin{rail}
    2.11 -  ('theory' | 'theory\_ref') nameref?
    2.12 +  'theory' nameref?
    2.13    ;
    2.14    \end{rail}
    2.15  
    2.16 @@ -243,10 +242,6 @@
    2.17    theory @{text "A"} of the background theory of the current context
    2.18    --- as abstract value.
    2.19  
    2.20 -  \item @{text "@{theory_ref}"} is similar to @{text "@{theory}"}, but
    2.21 -  produces a @{ML_type theory_ref} via @{ML "Theory.check_thy"} as
    2.22 -  explained above.
    2.23 -
    2.24    \end{description}
    2.25  *}
    2.26  
     3.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Fri Oct 29 11:04:41 2010 +0200
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Fri Oct 29 11:07:21 2010 +0200
     3.3 @@ -262,11 +262,10 @@
     3.4  \begin{isamarkuptext}%
     3.5  \begin{matharray}{rcl}
     3.6    \indexdef{}{ML antiquotation}{theory}\hypertarget{ML antiquotation.theory}{\hyperlink{ML antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
     3.7 -  \indexdef{}{ML antiquotation}{theory\_ref}\hypertarget{ML antiquotation.theory-ref}{\hyperlink{ML antiquotation.theory-ref}{\mbox{\isa{theory{\isacharunderscore}ref}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
     3.8    \end{matharray}
     3.9  
    3.10    \begin{rail}
    3.11 -  ('theory' | 'theory\_ref') nameref?
    3.12 +  'theory' nameref?
    3.13    ;
    3.14    \end{rail}
    3.15  
    3.16 @@ -279,10 +278,6 @@
    3.17    theory \isa{A} of the background theory of the current context
    3.18    --- as abstract value.
    3.19  
    3.20 -  \item \isa{{\isacharat}{\isacharbraceleft}theory{\isacharunderscore}ref{\isacharbraceright}} is similar to \isa{{\isacharat}{\isacharbraceleft}theory{\isacharbraceright}}, but
    3.21 -  produces a \verb|theory_ref| via \verb|Theory.check_thy| as
    3.22 -  explained above.
    3.23 -
    3.24    \end{description}%
    3.25  \end{isamarkuptext}%
    3.26  \isamarkuptrue%
     4.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Fri Oct 29 11:04:41 2010 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Fri Oct 29 11:07:21 2010 +0200
     4.3 @@ -159,7 +159,7 @@
     4.4  
     4.5  text {*
     4.6    \begin{matharray}{rcll}
     4.7 -    @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!)\\
     4.8 +    @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
     4.9      @{command_def "definition"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    4.10      @{attribute_def "defn"} & : & @{text attribute} \\
    4.11      @{command_def "abbreviation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    4.12 @@ -1139,8 +1139,8 @@
    4.13    asserted, and records within the internal derivation object how
    4.14    presumed theorems depend on unproven suppositions.
    4.15  
    4.16 -  \begin{matharray}{rcl}
    4.17 -    @{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} \\
    4.18 +  \begin{matharray}{rcll}
    4.19 +    @{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
    4.20    \end{matharray}
    4.21  
    4.22    \begin{rail}
    4.23 @@ -1159,7 +1159,7 @@
    4.24  
    4.25    \end{description}
    4.26  
    4.27 -  See @{"file" "~~/src/FOL/ex/Iff_Oracle.thy"} for a worked example of
    4.28 +  See @{"file" "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of
    4.29    defining a new primitive rule as oracle, and turning it into a proof
    4.30    method.
    4.31  *}
     5.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Fri Oct 29 11:04:41 2010 +0200
     5.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Fri Oct 29 11:07:21 2010 +0200
     5.3 @@ -179,7 +179,7 @@
     5.4  %
     5.5  \begin{isamarkuptext}%
     5.6  \begin{matharray}{rcll}
     5.7 -    \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!)\\
     5.8 +    \indexdef{}{command}{axiomatization}\hypertarget{command.axiomatization}{\hyperlink{command.axiomatization}{\mbox{\isa{\isacommand{axiomatization}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
     5.9      \indexdef{}{command}{definition}\hypertarget{command.definition}{\hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
    5.10      \indexdef{}{attribute}{defn}\hypertarget{attribute.defn}{\hyperlink{attribute.defn}{\mbox{\isa{defn}}}} & : & \isa{attribute} \\
    5.11      \indexdef{}{command}{abbreviation}\hypertarget{command.abbreviation}{\hyperlink{command.abbreviation}{\mbox{\isa{\isacommand{abbreviation}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
    5.12 @@ -1179,8 +1179,8 @@
    5.13    asserted, and records within the internal derivation object how
    5.14    presumed theorems depend on unproven suppositions.
    5.15  
    5.16 -  \begin{matharray}{rcl}
    5.17 -    \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
    5.18 +  \begin{matharray}{rcll}
    5.19 +    \indexdef{}{command}{oracle}\hypertarget{command.oracle}{\hyperlink{command.oracle}{\mbox{\isa{\isacommand{oracle}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
    5.20    \end{matharray}
    5.21  
    5.22    \begin{rail}
    5.23 @@ -1199,7 +1199,7 @@
    5.24  
    5.25    \end{description}
    5.26  
    5.27 -  See \hyperlink{file.~~/src/FOL/ex/Iff-Oracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}FOL{\isacharslash}ex{\isacharslash}Iff{\isacharunderscore}Oracle{\isachardot}thy}}}} for a worked example of
    5.28 +  See \hyperlink{file.~~/src/HOL/ex/Iff-Oracle.thy}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}HOL{\isacharslash}ex{\isacharslash}Iff{\isacharunderscore}Oracle{\isachardot}thy}}}} for a worked example of
    5.29    defining a new primitive rule as oracle, and turning it into a proof
    5.30    method.%
    5.31  \end{isamarkuptext}%
     6.1 --- a/src/FOL/IsaMakefile	Fri Oct 29 11:04:41 2010 +0200
     6.2 +++ b/src/FOL/IsaMakefile	Fri Oct 29 11:07:21 2010 +0200
     6.3 @@ -45,14 +45,13 @@
     6.4  FOL-ex: FOL $(LOG)/FOL-ex.gz
     6.5  
     6.6  $(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy		\
     6.7 -  ex/Iff_Oracle.thy ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy	\
     6.8 +  ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy			\
     6.9    ex/Locale_Test/Locale_Test.thy ex/Locale_Test/Locale_Test1.thy	\
    6.10    ex/Locale_Test/Locale_Test2.thy ex/Locale_Test/Locale_Test3.thy	\
    6.11 -  ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML				\
    6.12 -  ex/Classical.thy ex/document/root.tex ex/Foundation.thy		\
    6.13 -  ex/Intuitionistic.thy ex/Intro.thy ex/Propositional_Int.thy		\
    6.14 -  ex/Propositional_Cla.thy ex/Quantifiers_Int.thy			\
    6.15 -  ex/Quantifiers_Cla.thy
    6.16 +  ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML ex/Classical.thy		\
    6.17 +  ex/document/root.tex ex/Foundation.thy ex/Intuitionistic.thy		\
    6.18 +  ex/Intro.thy ex/Propositional_Int.thy ex/Propositional_Cla.thy	\
    6.19 +  ex/Quantifiers_Int.thy ex/Quantifiers_Cla.thy
    6.20  	@$(ISABELLE_TOOL) usedir $(OUT)/FOL ex
    6.21  
    6.22  
     7.1 --- a/src/FOL/ex/Iff_Oracle.thy	Fri Oct 29 11:04:41 2010 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,76 +0,0 @@
     7.4 -(*  Title:      FOL/ex/Iff_Oracle.thy
     7.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.6 -    Copyright   1996  University of Cambridge
     7.7 -*)
     7.8 -
     7.9 -header {* Example of Declaring an Oracle *}
    7.10 -
    7.11 -theory Iff_Oracle
    7.12 -imports FOL
    7.13 -begin
    7.14 -
    7.15 -subsection {* Oracle declaration *}
    7.16 -
    7.17 -text {*
    7.18 -  This oracle makes tautologies of the form @{text "P <-> P <-> P <-> P"}.
    7.19 -  The length is specified by an integer, which is checked to be even
    7.20 -  and positive.
    7.21 -*}
    7.22 -
    7.23 -oracle iff_oracle = {*
    7.24 -  let
    7.25 -    fun mk_iff 1 = Var (("P", 0), @{typ o})
    7.26 -      | mk_iff n = FOLogic.iff $ Var (("P", 0), @{typ o}) $ mk_iff (n - 1);
    7.27 -  in
    7.28 -    fn (thy, n) =>
    7.29 -      if n > 0 andalso n mod 2 = 0
    7.30 -      then Thm.cterm_of thy (FOLogic.mk_Trueprop (mk_iff n))
    7.31 -      else raise Fail ("iff_oracle: " ^ string_of_int n)
    7.32 -  end
    7.33 -*}
    7.34 -
    7.35 -
    7.36 -subsection {* Oracle as low-level rule *}
    7.37 -
    7.38 -ML {* iff_oracle (@{theory}, 2) *}
    7.39 -ML {* iff_oracle (@{theory}, 10) *}
    7.40 -ML {* Thm.proof_body_of (iff_oracle (@{theory}, 10)) *}
    7.41 -
    7.42 -text {* These oracle calls had better fail. *}
    7.43 -
    7.44 -ML {*
    7.45 -  (iff_oracle (@{theory}, 5); error "?")
    7.46 -    handle Fail _ => warning "Oracle failed, as expected"
    7.47 -*}
    7.48 -
    7.49 -ML {*
    7.50 -  (iff_oracle (@{theory}, 1); error "?")
    7.51 -    handle Fail _ => warning "Oracle failed, as expected"
    7.52 -*}
    7.53 -
    7.54 -
    7.55 -subsection {* Oracle as proof method *}
    7.56 -
    7.57 -method_setup iff = {*
    7.58 -  Scan.lift Parse.nat >> (fn n => fn ctxt =>
    7.59 -    SIMPLE_METHOD
    7.60 -      (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
    7.61 -        handle Fail _ => no_tac))
    7.62 -*} "iff oracle"
    7.63 -
    7.64 -
    7.65 -lemma "A <-> A"
    7.66 -  by (iff 2)
    7.67 -
    7.68 -lemma "A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A"
    7.69 -  by (iff 10)
    7.70 -
    7.71 -lemma "A <-> A <-> A <-> A <-> A"
    7.72 -  apply (iff 5)?
    7.73 -  oops
    7.74 -
    7.75 -lemma A
    7.76 -  apply (iff 1)?
    7.77 -  oops
    7.78 -
    7.79 -end
     8.1 --- a/src/FOL/ex/ROOT.ML	Fri Oct 29 11:04:41 2010 +0200
     8.2 +++ b/src/FOL/ex/ROOT.ML	Fri Oct 29 11:07:21 2010 +0200
     8.3 @@ -18,8 +18,7 @@
     8.4    "Propositional_Cla",
     8.5    "Quantifiers_Cla",
     8.6    "Miniscope",
     8.7 -  "If",
     8.8 -  "Iff_Oracle"
     8.9 +  "If"
    8.10  ];
    8.11  
    8.12  (*regression test for locales -- sets several global flags!*)
     9.1 --- a/src/HOL/IsaMakefile	Fri Oct 29 11:04:41 2010 +0200
     9.2 +++ b/src/HOL/IsaMakefile	Fri Oct 29 11:07:21 2010 +0200
     9.3 @@ -1016,20 +1016,19 @@
     9.4    ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy		\
     9.5    ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy		\
     9.6    ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy	\
     9.7 -  ex/Induction_Schema.thy ex/InductiveInvariant.thy			\
     9.8 +  ex/Iff_Oracle.thy ex/Induction_Schema.thy ex/InductiveInvariant.thy	\
     9.9    ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy		\
    9.10    ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy		\
    9.11    ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy	\
    9.12 -  ex/Normalization_by_Evaluation.thy					\
    9.13 -  ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy		\
    9.14 -  ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy		\
    9.15 -  ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy		\
    9.16 -  ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
    9.17 -  ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy		\
    9.18 -  ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy	\
    9.19 -  ex/Unification.thy ex/While_Combinator_Example.thy			\
    9.20 -  ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML	\
    9.21 -  ex/svc_test.thy
    9.22 +  ex/Normalization_by_Evaluation.thy ex/Numeral.thy ex/PER.thy		\
    9.23 +  ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy		\
    9.24 +  ex/Quickcheck_Lattice_Examples.thy ex/ROOT.ML ex/Recdefs.thy		\
    9.25 +  ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy		\
    9.26 +  ex/SAT_Examples.thy ex/SVC_Oracle.thy ex/Serbian.thy ex/Sqrt.thy	\
    9.27 +  ex/Sqrt_Script.thy ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy	\
    9.28 +  ex/Transfer_Ex.thy ex/Tree23.thy ex/Unification.thy			\
    9.29 +  ex/While_Combinator_Example.thy ex/document/root.bib			\
    9.30 +  ex/document/root.tex ex/set.thy ex/svc_funcs.ML ex/svc_test.thy
    9.31  	@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
    9.32  
    9.33  
    10.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 29 11:04:41 2010 +0200
    10.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 29 11:07:21 2010 +0200
    10.3 @@ -703,7 +703,7 @@
    10.4      val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
    10.5      val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
    10.6        if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
    10.7 -      else raise exn;
    10.8 +      else reraise exn;
    10.9  
   10.10      val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
   10.11  
    11.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Fri Oct 29 11:04:41 2010 +0200
    11.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Fri Oct 29 11:07:21 2010 +0200
    11.3 @@ -6,10 +6,11 @@
    11.4  
    11.5  signature QUOTIENT_INFO =
    11.6  sig
    11.7 -  exception NotFound
    11.8 +  exception NotFound  (* FIXME complicates signatures unnecessarily *)
    11.9  
   11.10    type maps_info = {mapfun: string, relmap: string}
   11.11    val maps_defined: theory -> string -> bool
   11.12 +  (* FIXME functions called "lookup" must return option, not raise exception *)
   11.13    val maps_lookup: theory -> string -> maps_info     (* raises NotFound *)
   11.14    val maps_update_thy: string -> maps_info -> theory -> theory
   11.15    val maps_update: string -> maps_info -> Proof.context -> Proof.context
    12.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Fri Oct 29 11:04:41 2010 +0200
    12.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Fri Oct 29 11:07:21 2010 +0200
    12.3 @@ -67,8 +67,8 @@
    12.4  fun get_mapfun ctxt s =
    12.5  let
    12.6    val thy = ProofContext.theory_of ctxt
    12.7 -  val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
    12.8 -  val mapfun = #mapfun (maps_lookup thy s) handle NotFound => raise exn
    12.9 +  val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound =>
   12.10 +    raise LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
   12.11  in
   12.12    Const (mapfun, dummyT)
   12.13  end
   12.14 @@ -104,8 +104,8 @@
   12.15  fun get_rty_qty ctxt s =
   12.16  let
   12.17    val thy = ProofContext.theory_of ctxt
   12.18 -  val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
   12.19 -  val qdata = quotdata_lookup thy s handle NotFound => raise exn
   12.20 +  val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound =>
   12.21 +    raise LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
   12.22  in
   12.23    (#rtyp qdata, #qtyp qdata)
   12.24  end
   12.25 @@ -127,7 +127,7 @@
   12.26    val thy = ProofContext.theory_of ctxt
   12.27  in
   12.28    Sign.typ_match thy (ty_pat, ty) Vartab.empty
   12.29 -  handle MATCH_TYPE => err ctxt ty_pat ty
   12.30 +  handle Type.TYPE_MATCH => err ctxt ty_pat ty
   12.31  end
   12.32  
   12.33  (* produces the rep or abs constant for a qty *)
   12.34 @@ -276,8 +276,8 @@
   12.35  fun get_relmap ctxt s =
   12.36  let
   12.37    val thy = ProofContext.theory_of ctxt
   12.38 -  val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
   12.39 -  val relmap = #relmap (maps_lookup thy s) handle NotFound => raise exn
   12.40 +  val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound =>
   12.41 +    raise LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
   12.42  in
   12.43    Const (relmap, dummyT)
   12.44  end
   12.45 @@ -299,9 +299,9 @@
   12.46  fun get_equiv_rel ctxt s =
   12.47  let
   12.48    val thy = ProofContext.theory_of ctxt
   12.49 -  val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
   12.50  in
   12.51 -  #equiv_rel (quotdata_lookup thy s) handle NotFound => raise exn
   12.52 +  #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound =>
   12.53 +    raise LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
   12.54  end
   12.55  
   12.56  fun equiv_match_err ctxt ty_pat ty =
   12.57 @@ -563,7 +563,8 @@
   12.58           else
   12.59             let
   12.60               val rtrm' = #rconst (qconsts_lookup thy qtrm)
   12.61 -               handle NotFound => term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
   12.62 +               handle Quotient_Info.NotFound =>
   12.63 +                term_mismatch "regularize (constant not found)" ctxt rtrm qtrm
   12.64             in
   12.65               if Pattern.matches thy (rtrm', rtrm)
   12.66               then rtrm else term_mismatch "regularize (constant mismatch)" ctxt rtrm qtrm
    13.1 --- a/src/HOL/Tools/sat_funcs.ML	Fri Oct 29 11:04:41 2010 +0200
    13.2 +++ b/src/HOL/Tools/sat_funcs.ML	Fri Oct 29 11:07:21 2010 +0200
    13.3 @@ -274,22 +274,6 @@
    13.4    | string_of_prop_formula (PropLogic.And (fm1, fm2)) = "(" ^ string_of_prop_formula fm1 ^ " & " ^ string_of_prop_formula fm2 ^ ")";
    13.5  
    13.6  (* ------------------------------------------------------------------------- *)
    13.7 -(* take_prefix:                                                              *)
    13.8 -(*      take_prefix n [x_1, ..., x_k] = ([x_1, ..., x_n], [x_n+1, ..., x_k]) *)
    13.9 -(* ------------------------------------------------------------------------- *)
   13.10 -
   13.11 -(* int -> 'a list -> 'a list * 'a list *)
   13.12 -
   13.13 -fun take_prefix n xs =
   13.14 -let
   13.15 -	fun take 0 (rxs, xs)      = (rev rxs, xs)
   13.16 -	  | take _ (rxs, [])      = (rev rxs, [])
   13.17 -	  | take n (rxs, x :: xs) = take (n-1) (x :: rxs, xs)
   13.18 -in
   13.19 -	take n ([], xs)
   13.20 -end;
   13.21 -
   13.22 -(* ------------------------------------------------------------------------- *)
   13.23  (* rawsat_thm: run external SAT solver with the given clauses.  Reconstructs *)
   13.24  (*      a proof from the resulting proof trace of the SAT solver.  The       *)
   13.25  (*      theorem returned is just "False" (with some of the given clauses as  *)
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/ex/Iff_Oracle.thy	Fri Oct 29 11:07:21 2010 +0200
    14.3 @@ -0,0 +1,76 @@
    14.4 +(*  Title:      HOL/ex/Iff_Oracle.thy
    14.5 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    14.6 +    Author:     Makarius
    14.7 +*)
    14.8 +
    14.9 +header {* Example of Declaring an Oracle *}
   14.10 +
   14.11 +theory Iff_Oracle
   14.12 +imports Main
   14.13 +begin
   14.14 +
   14.15 +subsection {* Oracle declaration *}
   14.16 +
   14.17 +text {*
   14.18 +  This oracle makes tautologies of the form @{prop "P <-> P <-> P <-> P"}.
   14.19 +  The length is specified by an integer, which is checked to be even
   14.20 +  and positive.
   14.21 +*}
   14.22 +
   14.23 +oracle iff_oracle = {*
   14.24 +  let
   14.25 +    fun mk_iff 1 = Var (("P", 0), @{typ bool})
   14.26 +      | mk_iff n = HOLogic.mk_eq (Var (("P", 0), @{typ bool}), mk_iff (n - 1));
   14.27 +  in
   14.28 +    fn (thy, n) =>
   14.29 +      if n > 0 andalso n mod 2 = 0
   14.30 +      then Thm.cterm_of thy (HOLogic.mk_Trueprop (mk_iff n))
   14.31 +      else raise Fail ("iff_oracle: " ^ string_of_int n)
   14.32 +  end
   14.33 +*}
   14.34 +
   14.35 +
   14.36 +subsection {* Oracle as low-level rule *}
   14.37 +
   14.38 +ML {* iff_oracle (@{theory}, 2) *}
   14.39 +ML {* iff_oracle (@{theory}, 10) *}
   14.40 +ML {* Thm.status_of (iff_oracle (@{theory}, 10)) *}
   14.41 +
   14.42 +text {* These oracle calls had better fail. *}
   14.43 +
   14.44 +ML {*
   14.45 +  (iff_oracle (@{theory}, 5); error "Bad oracle")
   14.46 +    handle Fail _ => warning "Oracle failed, as expected"
   14.47 +*}
   14.48 +
   14.49 +ML {*
   14.50 +  (iff_oracle (@{theory}, 1); error "Bad oracle")
   14.51 +    handle Fail _ => warning "Oracle failed, as expected"
   14.52 +*}
   14.53 +
   14.54 +
   14.55 +subsection {* Oracle as proof method *}
   14.56 +
   14.57 +method_setup iff = {*
   14.58 +  Scan.lift Parse.nat >> (fn n => fn ctxt =>
   14.59 +    SIMPLE_METHOD
   14.60 +      (HEADGOAL (rtac (iff_oracle (ProofContext.theory_of ctxt, n)))
   14.61 +        handle Fail _ => no_tac))
   14.62 +*} "iff oracle"
   14.63 +
   14.64 +
   14.65 +lemma "A <-> A"
   14.66 +  by (iff 2)
   14.67 +
   14.68 +lemma "A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A <-> A"
   14.69 +  by (iff 10)
   14.70 +
   14.71 +lemma "A <-> A <-> A <-> A <-> A"
   14.72 +  apply (iff 5)?
   14.73 +  oops
   14.74 +
   14.75 +lemma A
   14.76 +  apply (iff 1)?
   14.77 +  oops
   14.78 +
   14.79 +end
    15.1 --- a/src/HOL/ex/ROOT.ML	Fri Oct 29 11:04:41 2010 +0200
    15.2 +++ b/src/HOL/ex/ROOT.ML	Fri Oct 29 11:07:21 2010 +0200
    15.3 @@ -12,6 +12,7 @@
    15.4  ];
    15.5  
    15.6  use_thys [
    15.7 +  "Iff_Oracle",
    15.8    "Numeral",
    15.9    "Higher_Order_Logic",
   15.10    "Abstract_NAT",
    16.1 --- a/src/Pure/Concurrent/simple_thread.ML	Fri Oct 29 11:04:41 2010 +0200
    16.2 +++ b/src/Pure/Concurrent/simple_thread.ML	Fri Oct 29 11:07:21 2010 +0200
    16.3 @@ -32,21 +32,21 @@
    16.4  fun synchronized name lock e =
    16.5    if Multithreading.available then
    16.6      Exn.release (uninterruptible (fn restore_attributes => fn () =>
    16.7 -    let
    16.8 -      val immediate =
    16.9 -        if Mutex.trylock lock then true
   16.10 -        else
   16.11 -          let
   16.12 -            val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ...");
   16.13 -            val time = Multithreading.real_time Mutex.lock lock;
   16.14 -            val _ = Multithreading.tracing_time true time
   16.15 -              (fn () => name ^ ": locked after " ^ Time.toString time);
   16.16 -          in false end;
   16.17 -      val result = Exn.capture (restore_attributes e) ();
   16.18 -      val _ =
   16.19 -        if immediate then () else Multithreading.tracing 5 (fn () => name ^ ": unlocking ...");
   16.20 -      val _ = Mutex.unlock lock;
   16.21 -    in result end) ())
   16.22 +      let
   16.23 +        val immediate =
   16.24 +          if Mutex.trylock lock then true
   16.25 +          else
   16.26 +            let
   16.27 +              val _ = Multithreading.tracing 5 (fn () => name ^ ": locking ...");
   16.28 +              val time = Multithreading.real_time Mutex.lock lock;
   16.29 +              val _ = Multithreading.tracing_time true time
   16.30 +                (fn () => name ^ ": locked after " ^ Time.toString time);
   16.31 +            in false end;
   16.32 +        val result = Exn.capture (restore_attributes e) ();
   16.33 +        val _ =
   16.34 +          if immediate then () else Multithreading.tracing 5 (fn () => name ^ ": unlocking ...");
   16.35 +        val _ = Mutex.unlock lock;
   16.36 +      in result end) ())
   16.37    else e ();
   16.38  
   16.39  end;
    17.1 --- a/src/Pure/General/exn.ML	Fri Oct 29 11:04:41 2010 +0200
    17.2 +++ b/src/Pure/General/exn.ML	Fri Oct 29 11:07:21 2010 +0200
    17.3 @@ -11,12 +11,13 @@
    17.4    val get_exn: 'a result -> exn option
    17.5    val capture: ('a -> 'b) -> 'a -> 'b result
    17.6    val release: 'a result -> 'a
    17.7 -  val map_result: ('a -> 'a) -> 'a result -> 'a result
    17.8 +  val map_result: ('a -> 'b) -> 'a result -> 'b result
    17.9    exception Interrupt
   17.10    val interrupt: unit -> 'a
   17.11    val is_interrupt: exn -> bool
   17.12    val interrupt_exn: 'a result
   17.13    val is_interrupt_exn: 'a result -> bool
   17.14 +  val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
   17.15    exception EXCEPTIONS of exn list
   17.16    val flatten: exn -> exn list
   17.17    val flatten_list: exn list -> exn list
   17.18 @@ -45,7 +46,7 @@
   17.19    | release (Exn e) = reraise e;
   17.20  
   17.21  fun map_result f (Result x) = Result (f x)
   17.22 -  | map_result f e = e;
   17.23 +  | map_result f (Exn e) = (Exn e);
   17.24  
   17.25  
   17.26  (* interrupts *)
   17.27 @@ -55,7 +56,7 @@
   17.28  fun interrupt () = raise Interrupt;
   17.29  
   17.30  fun is_interrupt Interrupt = true
   17.31 -  | is_interrupt (IO.Io {cause = Interrupt, ...}) = true
   17.32 +  | is_interrupt (IO.Io {cause, ...}) = is_interrupt cause
   17.33    | is_interrupt _ = false;
   17.34  
   17.35  val interrupt_exn = Exn Interrupt;
   17.36 @@ -63,6 +64,9 @@
   17.37  fun is_interrupt_exn (Exn exn) = is_interrupt exn
   17.38    | is_interrupt_exn _ = false;
   17.39  
   17.40 +fun interruptible_capture f x =
   17.41 +  Result (f x) handle e => if is_interrupt e then reraise e else Exn e;
   17.42 +
   17.43  
   17.44  (* nested exceptions *)
   17.45  
    18.1 --- a/src/Pure/IsaMakefile	Fri Oct 29 11:04:41 2010 +0200
    18.2 +++ b/src/Pure/IsaMakefile	Fri Oct 29 11:07:21 2010 +0200
    18.3 @@ -20,6 +20,7 @@
    18.4  ## Pure
    18.5  
    18.6  BOOTSTRAP_FILES = 					\
    18.7 +  General/exn.ML					\
    18.8    ML-Systems/bash.ML 					\
    18.9    ML-Systems/compiler_polyml-5.2.ML			\
   18.10    ML-Systems/compiler_polyml-5.3.ML			\
   18.11 @@ -73,7 +74,6 @@
   18.12    General/basics.ML					\
   18.13    General/binding.ML					\
   18.14    General/buffer.ML					\
   18.15 -  General/exn.ML					\
   18.16    General/file.ML					\
   18.17    General/graph.ML					\
   18.18    General/heap.ML					\
    19.1 --- a/src/Pure/Isar/local_defs.ML	Fri Oct 29 11:04:41 2010 +0200
    19.2 +++ b/src/Pure/Isar/local_defs.ML	Fri Oct 29 11:07:21 2010 +0200
    19.3 @@ -44,8 +44,9 @@
    19.4  
    19.5  fun cert_def ctxt eq =
    19.6    let
    19.7 -    fun err msg = cat_error msg ("The error(s) above occurred in definition: " ^
    19.8 -      quote (Syntax.string_of_term ctxt eq));
    19.9 +    fun err msg =
   19.10 +      cat_error msg ("The error(s) above occurred in definition:\n" ^
   19.11 +        quote (Syntax.string_of_term ctxt eq));
   19.12      val ((lhs, _), eq') = eq
   19.13        |> Sign.no_vars ctxt
   19.14        |> Primitive_Defs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
   19.15 @@ -245,7 +246,7 @@
   19.16            (CONVERSION (meta_rewrite_conv ctxt') THEN'
   19.17              MetaSimplifier.rewrite_goal_tac [def] THEN'
   19.18              resolve_tac [Drule.reflexive_thm])))
   19.19 -        handle ERROR msg => cat_error msg "Failed to prove definitional specification."
   19.20 +        handle ERROR msg => cat_error msg "Failed to prove definitional specification"
   19.21        end;
   19.22    in (((c, T), rhs), prove) end;
   19.23  
    20.1 --- a/src/Pure/ML/ml_antiquote.ML	Fri Oct 29 11:04:41 2010 +0200
    20.2 +++ b/src/Pure/ML/ml_antiquote.ML	Fri Oct 29 11:07:21 2010 +0200
    20.3 @@ -71,12 +71,6 @@
    20.4      "Context.get_theory (ML_Context.the_global_context ()) " ^ ML_Syntax.print_string name)
    20.5    || Scan.succeed "ML_Context.the_global_context ()");
    20.6  
    20.7 -val _ = value "theory_ref"
    20.8 -  (Scan.lift Args.name >> (fn name =>
    20.9 -    "Theory.check_thy (Context.get_theory (ML_Context.the_global_context ()) " ^
   20.10 -      ML_Syntax.print_string name ^ ")")
   20.11 -  || Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");
   20.12 -
   20.13  val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
   20.14  
   20.15  val _ = inline "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
    21.1 --- a/src/Pure/Syntax/syn_trans.ML	Fri Oct 29 11:04:41 2010 +0200
    21.2 +++ b/src/Pure/Syntax/syn_trans.ML	Fri Oct 29 11:07:21 2010 +0200
    21.3 @@ -547,7 +547,7 @@
    21.4      fun ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
    21.5        | ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
    21.6  
    21.7 -    val exn_results = map (Exn.capture ast_of) pts;
    21.8 +    val exn_results = map (Exn.interruptible_capture ast_of) pts;
    21.9      val exns = map_filter Exn.get_exn exn_results;
   21.10      val results = map_filter Exn.get_result exn_results
   21.11    in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
   21.12 @@ -571,7 +571,7 @@
   21.13            Term.list_comb (term_of ast, map term_of asts)
   21.14        | term_of (ast as Ast.Appl _) = raise Ast.AST ("ast_to_term: malformed ast", [ast]);
   21.15  
   21.16 -    val exn_results = map (Exn.capture term_of) asts;
   21.17 +    val exn_results = map (Exn.interruptible_capture term_of) asts;
   21.18      val exns = map_filter Exn.get_exn exn_results;
   21.19      val results = map_filter Exn.get_result exn_results
   21.20    in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
    22.1 --- a/src/Pure/more_thm.ML	Fri Oct 29 11:04:41 2010 +0200
    22.2 +++ b/src/Pure/more_thm.ML	Fri Oct 29 11:07:21 2010 +0200
    22.3 @@ -12,6 +12,7 @@
    22.4    structure Ctermtab: TABLE
    22.5    structure Thmtab: TABLE
    22.6    val aconvc: cterm * cterm -> bool
    22.7 +  type attribute = Context.generic * thm -> Context.generic * thm
    22.8  end;
    22.9  
   22.10  signature THM =
   22.11 @@ -64,6 +65,7 @@
   22.12    val close_derivation: thm -> thm
   22.13    val add_axiom: binding * term -> theory -> (string * thm) * theory
   22.14    val add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory
   22.15 +  type attribute = Context.generic * thm -> Context.generic * thm
   22.16    type binding = binding * attribute list
   22.17    val empty_binding: binding
   22.18    val rule_attribute: (Context.generic -> thm -> thm) -> attribute
   22.19 @@ -382,6 +384,9 @@
   22.20  
   22.21  (** attributes **)
   22.22  
   22.23 +(*attributes subsume any kind of rules or context modifiers*)
   22.24 +type attribute = Context.generic * thm -> Context.generic * thm;
   22.25 +
   22.26  type binding = binding * attribute list;
   22.27  val empty_binding: binding = (Binding.empty, []);
   22.28  
    23.1 --- a/src/Pure/thm.ML	Fri Oct 29 11:04:41 2010 +0200
    23.2 +++ b/src/Pure/thm.ML	Fri Oct 29 11:07:21 2010 +0200
    23.3 @@ -39,7 +39,6 @@
    23.4    (*theorems*)
    23.5    type thm
    23.6    type conv = cterm -> thm
    23.7 -  type attribute = Context.generic * thm -> Context.generic * thm
    23.8    val rep_thm: thm ->
    23.9     {thy_ref: theory_ref,
   23.10      tags: Properties.T,
   23.11 @@ -350,9 +349,6 @@
   23.12  
   23.13  type conv = cterm -> thm;
   23.14  
   23.15 -(*attributes subsume any kind of rules or context modifiers*)
   23.16 -type attribute = Context.generic * thm -> Context.generic * thm;
   23.17 -
   23.18  (*errors involving theorems*)
   23.19  exception THM of string * int * thm list;
   23.20  
    24.1 --- a/src/Tools/Code/code_runtime.ML	Fri Oct 29 11:04:41 2010 +0200
    24.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Oct 29 11:07:21 2010 +0200
    24.3 @@ -105,7 +105,7 @@
    24.4      val (program_code, [SOME value_name']) = serializer naming program' [value_name];
    24.5      val value_code = space_implode " "
    24.6        (value_name' :: "()" :: map (enclose "(" ")") args);
    24.7 -  in Exn.capture (value ctxt cookie) (program_code, value_code) end;
    24.8 +  in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
    24.9  
   24.10  fun partiality_as_none e = SOME (Exn.release e)
   24.11    handle General.Match => NONE
    25.1 --- a/src/Tools/quickcheck.ML	Fri Oct 29 11:04:41 2010 +0200
    25.2 +++ b/src/Tools/quickcheck.ML	Fri Oct 29 11:07:21 2010 +0200
    25.3 @@ -170,9 +170,10 @@
    25.4  
    25.5  fun mk_testers_strict ctxt t =
    25.6    let
    25.7 -    val generators = ((map snd o fst o Data.get  o Context.Proof) ctxt)
    25.8 -    val testers = map (fn generator => Exn.capture (generator ctxt) t) generators;
    25.9 -  in if forall (is_none o Exn.get_result) testers
   25.10 +    val generators = ((map snd o fst o Data.get o Context.Proof) ctxt)
   25.11 +    val testers = map (fn generator => Exn.interruptible_capture (generator ctxt) t) generators;
   25.12 +  in
   25.13 +    if forall (is_none o Exn.get_result) testers
   25.14      then [(Exn.release o snd o split_last) testers]
   25.15      else map_filter Exn.get_result testers
   25.16    end;
    26.1 --- a/src/ZF/simpdata.ML	Fri Oct 29 11:04:41 2010 +0200
    26.2 +++ b/src/ZF/simpdata.ML	Fri Oct 29 11:07:21 2010 +0200
    26.3 @@ -59,10 +59,10 @@
    26.4  
    26.5  in
    26.6  
    26.7 -val defBEX_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref})
    26.8 +val defBEX_regroup = Simplifier.simproc_global @{theory}
    26.9    "defined BEX" ["EX x:A. P(x) & Q(x)"] rearrange_bex;
   26.10  
   26.11 -val defBALL_regroup = Simplifier.simproc_global (Theory.deref @{theory_ref})
   26.12 +val defBALL_regroup = Simplifier.simproc_global @{theory}
   26.13    "defined BALL" ["ALL x:A. P(x) --> Q(x)"] rearrange_ball;
   26.14  
   26.15  end;