--- a/Admin/isatest/isatest-makedist Sat Oct 03 12:05:40 2009 +0200
+++ b/Admin/isatest/isatest-makedist Sat Oct 03 12:10:16 2009 +0200
@@ -106,7 +106,7 @@
sleep 15
$SSH atbroy99 "$MAKEALL $HOME/settings/at64-poly"
sleep 15
-$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8; $MAKEALL $HOME/settings/mac-poly64-M4; $MAKEALL $HOME/settings/mac-poly64-M8"
+$SSH macbroy2 "$MAKEALL $HOME/settings/mac-poly64-M4; $MAKEALL $HOME/settings/mac-poly64-M8; $MAKEALL $HOME/settings/mac-poly-M4; $MAKEALL $HOME/settings/mac-poly-M8"
sleep 15
$SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly"
sleep 15
--- a/Admin/isatest/settings/mac-poly64-M4 Sat Oct 03 12:05:40 2009 +0200
+++ b/Admin/isatest/settings/mac-poly64-M4 Sat Oct 03 12:10:16 2009 +0200
@@ -4,7 +4,7 @@
ML_SYSTEM="polyml-experimental"
ML_PLATFORM="x86_64-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="--mutable 5000 --immutable 2000"
+ ML_OPTIONS="--mutable 4000 --immutable 2000"
ISABELLE_HOME_USER=~/isabelle-mac-poly64-M4
--- a/Admin/isatest/settings/mac-poly64-M8 Sat Oct 03 12:05:40 2009 +0200
+++ b/Admin/isatest/settings/mac-poly64-M8 Sat Oct 03 12:10:16 2009 +0200
@@ -4,7 +4,7 @@
ML_SYSTEM="polyml-experimental"
ML_PLATFORM="x86_64-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="--mutable 5000 --immutable 2000"
+ ML_OPTIONS="--mutable 4000 --immutable 2000"
ISABELLE_HOME_USER=~/isabelle-mac-poly64-M8
--- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Sat Oct 03 12:05:40 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Sat Oct 03 12:10:16 2009 +0200
@@ -9,11 +9,11 @@
(* FIXME:
fun refute_action args timeout {pre=st, ...} =
let
- val subgoal = 0
+ val subgoal = 1
val thy = Proof.theory_of st
val thm = goal_thm_of st
- val refute = Refute.refute_subgoal thy args thm
+ val refute = Refute.refute_goal thy args thm
val _ = TimeLimit.timeLimit timeout refute subgoal
in
val writ_log = Substring.full (the (Symtab.lookup tab "writeln"))
--- a/src/HOL/Refute.thy Sat Oct 03 12:05:40 2009 +0200
+++ b/src/HOL/Refute.thy Sat Oct 03 12:10:16 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Refute.thy
- ID: $Id$
Author: Tjark Weber
Copyright 2003-2007
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Sat Oct 03 12:05:40 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Sat Oct 03 12:10:16 2009 +0200
@@ -91,7 +91,6 @@
);
fun lookup_thread xs = AList.lookup Thread.equal xs;
-fun delete_thread xs = AList.delete Thread.equal xs;
fun update_thread xs = AList.update Thread.equal xs;
@@ -117,7 +116,8 @@
(* unregister thread *)
fun unregister (success, message) thread = Synchronized.change state
- (fn state as State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+ (fn state as
+ State {managing_thread, timeout_heap, oldest_heap, active, cancelling, messages, store} =>
(case lookup_thread active thread of
SOME (birthtime, _, description) =>
let
@@ -317,9 +317,11 @@
fun print_provers thy = Pretty.writeln
(Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
-fun get_prover name thy = case Symtab.lookup (Provers.get thy) name of
- NONE => NONE
-| SOME (prover, _) => SOME prover;
+fun get_prover name thy =
+ (case Symtab.lookup (Provers.get thy) name of
+ NONE => NONE
+ | SOME (prover, _) => SOME prover);
+
(* start prover thread *)
--- a/src/HOL/Tools/lin_arith.ML Sat Oct 03 12:05:40 2009 +0200
+++ b/src/HOL/Tools/lin_arith.ML Sat Oct 03 12:10:16 2009 +0200
@@ -767,8 +767,6 @@
structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data);
-val map_data = Fast_Arith.map_data;
-
fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of};
--- a/src/HOL/Tools/old_primrec.ML Sat Oct 03 12:05:40 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML Sat Oct 03 12:10:16 2009 +0200
@@ -318,31 +318,7 @@
val add_primrec_unchecked = gen_primrec thy_note (thy_def true);
val add_primrec_i = gen_primrec_i thy_note (thy_def false);
val add_primrec_unchecked_i = gen_primrec_i thy_note (thy_def true);
-fun gen_primrec note def alt_name specs =
- gen_primrec_i note def alt_name (map (fn ((name, t), atts) => ((name, atts), t)) specs);
end;
-
-(* see primrec.ML (* outer syntax *)
-
-local structure P = OuterParse and K = OuterKeyword in
-
-val opt_unchecked_name =
- Scan.optional (P.$$$ "(" |-- P.!!!
- (((P.$$$ "unchecked" >> K true) -- Scan.optional P.name "" ||
- P.name >> pair false) --| P.$$$ ")")) (false, "");
-
-val primrec_decl =
- opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
-
-val _ =
- OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl
- (primrec_decl >> (fn ((unchecked, alt_name), eqns) =>
- Toplevel.theory (snd o
- (if unchecked then add_primrec_unchecked else add_primrec) alt_name
- (map P.triple_swap eqns))));
-
-end;*)
-
end;
--- a/src/HOL/Tools/recdef.ML Sat Oct 03 12:05:40 2009 +0200
+++ b/src/HOL/Tools/recdef.ML Sat Oct 03 12:10:16 2009 +0200
@@ -47,11 +47,6 @@
fun map_congs f = map_hints (fn (simps, congs, wfs) => (simps, f congs, wfs));
fun map_wfs f = map_hints (fn (simps, congs, wfs) => (simps, congs, f wfs));
-fun pretty_hints ({simps, congs, wfs}: hints) =
- [Pretty.big_list "recdef simp hints:" (map Display.pretty_thm_without_context simps),
- Pretty.big_list "recdef cong hints:" (map Display.pretty_thm_without_context (map snd congs)),
- Pretty.big_list "recdef wf hints:" (map Display.pretty_thm_without_context wfs)];
-
(* congruence rules *)
--- a/src/HOL/Tools/refute.ML Sat Oct 03 12:05:40 2009 +0200
+++ b/src/HOL/Tools/refute.ML Sat Oct 03 12:10:16 2009 +0200
@@ -51,9 +51,8 @@
(* tries to find a model for a formula: *)
val satisfy_term : theory -> (string * string) list -> Term.term -> unit
(* tries to find a model that refutes a formula: *)
- val refute_term : theory -> (string * string) list -> Term.term -> unit
- val refute_subgoal :
- theory -> (string * string) list -> Thm.thm -> int -> unit
+ val refute_term : theory -> (string * string) list -> term -> unit
+ val refute_goal : theory -> (string * string) list -> thm -> int -> unit
val setup : theory -> theory
@@ -1355,16 +1354,11 @@
end;
(* ------------------------------------------------------------------------- *)
-(* refute_subgoal: calls 'refute_term' on a specific subgoal *)
-(* params : list of '(name, value)' pairs used to override default *)
-(* parameters *)
-(* subgoal : 0-based index specifying the subgoal number *)
+(* refute_goal *)
(* ------------------------------------------------------------------------- *)
- (* theory -> (string * string) list -> Thm.thm -> int -> unit *)
-
- fun refute_subgoal thy params thm subgoal =
- refute_term thy params (List.nth (Thm.prems_of thm, subgoal));
+ fun refute_goal thy params st i =
+ refute_term thy params (Logic.get_goal (Thm.prop_of st) i);
(* ------------------------------------------------------------------------- *)
--- a/src/HOL/Tools/refute_isar.ML Sat Oct 03 12:05:40 2009 +0200
+++ b/src/HOL/Tools/refute_isar.ML Sat Oct 03 12:10:16 2009 +0200
@@ -1,106 +1,52 @@
(* Title: HOL/Tools/refute_isar.ML
- ID: $Id$
Author: Tjark Weber
Copyright 2003-2007
-Adds the 'refute' and 'refute_params' commands to Isabelle/Isar's outer
-syntax.
+Outer syntax commands 'refute' and 'refute_params'.
*)
-structure RefuteIsar: sig end =
+structure Refute_Isar: sig end =
struct
-(* ------------------------------------------------------------------------- *)
-(* common functions for argument parsing/scanning *)
-(* ------------------------------------------------------------------------- *)
-
-(* ------------------------------------------------------------------------- *)
-(* both 'refute' and 'refute_params' take an optional list of arguments of *)
-(* the form [name1=value1, name2=value2, ...] *)
-(* ------------------------------------------------------------------------- *)
+(* argument parsing *)
- val scan_parm = OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name);
+(*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
- val scan_parms = Scan.option
- (OuterParse.$$$ "[" |-- (OuterParse.list scan_parm) --| OuterParse.$$$ "]");
-
-(* ------------------------------------------------------------------------- *)
-(* set up the 'refute' command *)
-(* ------------------------------------------------------------------------- *)
+val scan_parm = OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name);
-(* ------------------------------------------------------------------------- *)
-(* 'refute' takes an optional list of parameters, followed by an optional *)
-(* subgoal number *)
-(* ------------------------------------------------------------------------- *)
-
- val refute_scan_args = scan_parms -- (Scan.option OuterParse.nat);
-
-(* ------------------------------------------------------------------------- *)
-(* the 'refute' command is mapped to 'Refute.refute_subgoal' *)
-(* ------------------------------------------------------------------------- *)
+val scan_parms = Scan.optional
+ (OuterParse.$$$ "[" |-- OuterParse.list scan_parm --| OuterParse.$$$ "]") [];
- fun refute_trans args =
- Toplevel.keep (fn state =>
- let
- val (parms_opt, subgoal_opt) = args
- val parms = Option.getOpt (parms_opt, [])
- val subgoal = Option.getOpt (subgoal_opt, 1) - 1
- val thy = Toplevel.theory_of state
- val thm = (snd o snd) (Proof.get_goal (Toplevel.proof_of state))
- in
- Refute.refute_subgoal thy parms thm subgoal
- end);
- fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans;
+(* 'refute' command *)
- val _ = OuterSyntax.improper_command "refute"
- "try to find a model that refutes a given subgoal"
- OuterKeyword.diag refute_parser;
-
-(* ------------------------------------------------------------------------- *)
-(* set up the 'refute_params' command *)
-(* ------------------------------------------------------------------------- *)
+val _ =
+ OuterSyntax.improper_command "refute"
+ "try to find a model that refutes a given subgoal" OuterKeyword.diag
+ (scan_parms -- Scan.optional OuterParse.nat 1 >>
+ (fn (parms, i) =>
+ Toplevel.keep (fn state =>
+ let
+ val thy = Toplevel.theory_of state;
+ val (_, st) = Proof.flat_goal (Toplevel.proof_of state);
+ in Refute.refute_goal thy parms st i end)));
-(* ------------------------------------------------------------------------- *)
-(* 'refute_params' takes an optional list of parameters *)
-(* ------------------------------------------------------------------------- *)
- val refute_params_scan_args = scan_parms;
-
-(* ------------------------------------------------------------------------- *)
-(* the 'refute_params' command is mapped to (multiple calls of) *)
-(* 'Refute.set_default_param'; then the (new) default parameters are *)
-(* displayed *)
-(* ------------------------------------------------------------------------- *)
+(* 'refute_params' command *)
- fun refute_params_trans args =
- let
- fun add_params thy [] =
- thy
- | add_params thy (p::ps) =
- add_params (Refute.set_default_param p thy) ps
- in
- Toplevel.theory (fn thy =>
- let
- val thy' = add_params thy (getOpt (args, []))
- val new_default_params = Refute.get_default_params thy'
- val output = if new_default_params=[] then
- "none"
- else
- cat_lines (map (fn (name, value) => name ^ "=" ^ value)
- new_default_params)
- in
- writeln ("Default parameters for 'refute':\n" ^ output);
- thy'
- end)
- end;
-
- fun refute_params_parser tokens =
- (refute_params_scan_args tokens) |>> refute_params_trans;
-
- val _ = OuterSyntax.command "refute_params"
- "show/store default parameters for the 'refute' command"
- OuterKeyword.thy_decl refute_params_parser;
+val _ =
+ OuterSyntax.command "refute_params"
+ "show/store default parameters for the 'refute' command" OuterKeyword.thy_decl
+ (scan_parms >> (fn parms =>
+ Toplevel.theory (fn thy =>
+ let
+ val thy' = fold Refute.set_default_param parms thy;
+ val output =
+ (case Refute.get_default_params thy' of
+ [] => "none"
+ | new_defaults => cat_lines (map (fn (x, y) => x ^ "=" ^ y) new_defaults));
+ val _ = writeln ("Default parameters for 'refute':\n" ^ output);
+ in thy' end)));
end;
--- a/src/Provers/clasimp.ML Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Provers/clasimp.ML Sat Oct 03 12:10:16 2009 +0200
@@ -141,7 +141,6 @@
val addXIs = modifier (ContextRules.intro_query NONE);
val addXEs = modifier (ContextRules.elim_query NONE);
-val addXDs = modifier (ContextRules.dest_query NONE);
val delXs = modifier ContextRules.rule_del;
in
@@ -266,9 +265,6 @@
HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (clasimpset_of ctxt)));
-fun clasimp_method tac =
- Args.bang_facts --| Method.sections clasimp_modifiers >> (clasimp_meth tac);
-
fun clasimp_method' tac =
Args.bang_facts --| Method.sections clasimp_modifiers >> (clasimp_meth' tac);
--- a/src/Provers/classical.ML Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Provers/classical.ML Sat Oct 03 12:10:16 2009 +0200
@@ -696,13 +696,13 @@
(*Backtracking is allowed among the various these unsafe ways of
proving a subgoal. *)
-fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) =
- assume_tac APPEND'
- contr_tac APPEND'
+fun inst0_step_tac (CS {safe0_netpair, ...}) =
+ assume_tac APPEND'
+ contr_tac APPEND'
biresolve_from_nets_tac safe0_netpair;
(*These unsafe steps could generate more subgoals.*)
-fun instp_step_tac (CS{safep_netpair,...}) =
+fun instp_step_tac (CS {safep_netpair, ...}) =
biresolve_from_nets_tac safep_netpair;
(*These steps could instantiate variables and are therefore unsafe.*)
@@ -768,7 +768,7 @@
(*Non-deterministic! Could always expand the first unsafe connective.
That's hard to implement and did not perform better in experiments, due to
greater search depth required.*)
-fun dup_step_tac (cs as (CS{dup_netpair,...})) =
+fun dup_step_tac (CS {dup_netpair, ...}) =
biresolve_from_nets_tac dup_netpair;
(*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*)
@@ -910,7 +910,6 @@
val introN = "intro";
val elimN = "elim";
val destN = "dest";
-val ruleN = "rule";
val setup_attrs =
Attrib.setup @{binding swapped} (Scan.succeed swapped)
--- a/src/Pure/Isar/isar_cmd.ML Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sat Oct 03 12:10:16 2009 +0200
@@ -450,14 +450,15 @@
Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss state args));
fun string_of_prfs full state arg =
- Pretty.string_of (case arg of
+ Pretty.string_of
+ (case arg of
NONE =>
let
- val (ctxt, (_, thm)) = Proof.get_goal state;
+ val (ctxt, thm) = Proof.flat_goal state;
val thy = ProofContext.theory_of ctxt;
val prf = Thm.proof_of thm;
val prop = Thm.full_prop_of thm;
- val prf' = Proofterm.rewrite_proof_notypes ([], []) prf
+ val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
in
ProofSyntax.pretty_proof ctxt
(if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
--- a/src/Pure/Isar/proof.ML Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Pure/Isar/proof.ML Sat Oct 03 12:10:16 2009 +0200
@@ -431,9 +431,7 @@
val refine = apply_text true;
val refine_end = apply_text false;
-
-fun refine_insert [] = I
- | refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths)));
+fun refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths)));
end;
--- a/src/Pure/Isar/specification.ML Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Pure/Isar/specification.ML Sat Oct 03 12:10:16 2009 +0200
@@ -286,7 +286,7 @@
val prems = Assumption.local_prems_of elems_ctxt ctxt;
val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt;
- in ((prems, stmt, []), goal_ctxt) end
+ in ((prems, stmt, NONE), goal_ctxt) end
| Element.Obtains obtains =>
let
val case_names = obtains |> map_index (fn (i, (b, _)) =>
@@ -327,7 +327,7 @@
|> fold_map assume_case (obtains ~~ propp)
|-> (fn ths => ProofContext.note_thmss Thm.assumptionK
[((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
- in ((prems, stmt, facts), goal_ctxt) end);
+ in ((prems, stmt, SOME facts), goal_ctxt) end);
structure TheoremHook = GenericDataFun
(
@@ -372,7 +372,7 @@
[((Binding.name AutoBind.assmsN, []), [(prems, [])])]
|> snd
|> Proof.theorem_i before_qed after_qed' (map snd stmt)
- |> Proof.refine_insert facts
+ |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
|> Library.apply (map (fn (f, _) => f int) (rev (TheoremHook.get (Context.Proof goal_ctxt))))
end;
--- a/src/Pure/Tools/find_theorems.ML Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML Sat Oct 03 12:10:16 2009 +0200
@@ -434,7 +434,7 @@
let
val proof_state = Toplevel.enter_proof_body state;
val ctxt = Proof.context_of proof_state;
- val opt_goal = try Proof.get_goal proof_state |> Option.map (#2 o #2);
+ val opt_goal = try Proof.flat_goal proof_state |> Option.map #2;
in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
local
--- a/src/Tools/auto_solve.ML Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Tools/auto_solve.ML Sat Oct 03 12:10:16 2009 +0200
@@ -16,7 +16,7 @@
val limit : int Unsynchronized.ref
end;
-structure AutoSolve : AUTO_SOLVE =
+structure Auto_Solve : AUTO_SOLVE =
struct
(* preferences *)
@@ -61,14 +61,14 @@
end;
fun seek_against_goal () =
- (case try Proof.get_goal state of
+ (case try Proof.flat_goal state of
NONE => NONE
- | SOME (_, (_, goal)) =>
+ | SOME (_, st) =>
let
- val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);
+ val subgoals = Drule.strip_imp_prems (Thm.cprop_of st);
val rs =
if length subgoals = 1
- then [(NONE, find goal)]
+ then [(NONE, find st)]
else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
val results = filter_out (null o snd) rs;
in if null results then NONE else SOME results end);
@@ -87,7 +87,7 @@
Pretty.markup Markup.hilite
(separate (Pretty.brk 0) (map prt_result results))])
| _ => state)
- end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
+ end handle TimeLimit.TimeOut => (warning "Auto solve: timeout"; state);
in
if int andalso ! auto andalso not (! Toplevel.quiet)
then go ()
@@ -96,6 +96,6 @@
end;
-val auto_solve = AutoSolve.auto;
-val auto_solve_time_limit = AutoSolve.auto_time_limit;
+val auto_solve = Auto_Solve.auto;
+val auto_solve_time_limit = Auto_Solve.auto_time_limit;
--- a/src/Tools/induct.ML Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Tools/induct.ML Sat Oct 03 12:10:16 2009 +0200
@@ -505,7 +505,6 @@
let
val thy = ProofContext.theory_of ctxt;
val cert = Thm.cterm_of thy;
- val certT = Thm.ctyp_of thy;
val v = Free (x, T);
fun spec_rule prfx (xs, body) =
@@ -579,7 +578,6 @@
fun induct_tac ctxt def_insts arbitrary taking opt_rule facts =
let
val thy = ProofContext.theory_of ctxt;
- val cert = Thm.cterm_of thy;
val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
@@ -652,7 +650,6 @@
fun coinduct_tac ctxt inst taking opt_rule facts =
let
val thy = ProofContext.theory_of ctxt;
- val cert = Thm.cterm_of thy;
fun inst_rule r =
if null inst then `RuleCases.get r
--- a/src/Tools/induct_tacs.ML Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Tools/induct_tacs.ML Sat Oct 03 12:10:16 2009 +0200
@@ -28,7 +28,7 @@
fun gen_case_tac ctxt0 s opt_rule i st =
let
- val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
+ val (_, ctxt) = Variable.focus_subgoal i st ctxt0;
val rule =
(case opt_rule of
SOME rule => rule
--- a/src/Tools/intuitionistic.ML Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Tools/intuitionistic.ML Sat Oct 03 12:10:16 2009 +0200
@@ -69,7 +69,6 @@
val introN = "intro";
val elimN = "elim";
val destN = "dest";
-val ruleN = "rule";
fun modifier name kind kind' att =
Args.$$$ name |-- (kind >> K NONE || kind' |-- OuterParse.nat --| Args.colon >> SOME)
--- a/src/Tools/quickcheck.ML Sat Oct 03 12:05:40 2009 +0200
+++ b/src/Tools/quickcheck.ML Sat Oct 03 12:10:16 2009 +0200
@@ -143,7 +143,7 @@
val thy = Proof.theory_of state;
fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
| strip t = t;
- val (_, (_, st)) = Proof.get_goal state;
+ val (_, st) = Proof.flat_goal state;
val (gi, frees) = Logic.goal_params (prop_of st) i;
val gi' = Logic.list_implies (assms, subst_bounds (frees, strip gi))
|> monomorphic_term thy insts default_T