1.1 --- a/src/Tools/quickcheck.ML	Fri Mar 02 09:35:35 2012 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Fri Mar 02 09:35:39 2012 +0100
     1.3 @@ -314,7 +314,27 @@
     1.4        tester ctxt (length testers > 1) insts goals |>
     1.5        (fn result => if exists found_counterexample result then SOME result else NONE)) testers)
     1.6        (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ();
     1.7 -      
     1.8 +
     1.9 +fun all_axioms_of ctxt t =
    1.10 +  let
    1.11 +    val intros = Locale.get_intros ctxt
    1.12 +    val unfolds = Locale.get_unfolds ctxt
    1.13 +    fun retrieve_prems thms t = 
    1.14 +       case filter (fn th => Term.could_unify (Thm.concl_of th, t)) thms of
    1.15 +         [] => NONE 
    1.16 +       | [th] =>
    1.17 +         let
    1.18 +           val (tyenv, tenv) =
    1.19 +             Pattern.match (Proof_Context.theory_of ctxt) (Thm.concl_of th, t) (Vartab.empty, Vartab.empty)
    1.20 +         in SOME (map (Envir.subst_term (tyenv, tenv)) (Thm.prems_of th)) end
    1.21 +    fun all t =
    1.22 +      case retrieve_prems intros t of
    1.23 +        NONE => retrieve_prems unfolds t
    1.24 +      | SOME ts => SOME (maps (fn t => the_default [t] (all t)) ts)
    1.25 +  in
    1.26 +    all t
    1.27 +  end
    1.28 +
    1.29  fun test_goal (time_limit, is_interactive) (insts, eval_terms) i state =
    1.30    let
    1.31      val lthy = Proof.context_of state;
    1.32 @@ -332,21 +352,17 @@
    1.33       of NONE => Assumption.all_assms_of lthy
    1.34        | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);
    1.35      val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
    1.36 -    fun assms_of locale = case fst (Locale.intros_of thy locale) of NONE => []
    1.37 -      | SOME th =>
    1.38 -          let
    1.39 -            val t = the_single (Assumption.all_assms_of (Locale.init locale thy))
    1.40 -            val (tyenv, tenv) =
    1.41 -              Pattern.match thy (concl_of th, term_of t) (Vartab.empty, Vartab.empty)
    1.42 -          in
    1.43 -            map (Envir.subst_term (tyenv, tenv)) (prems_of th)
    1.44 -          end
    1.45 +    fun axioms_of locale = case fst (Locale.specification_of thy locale) of
    1.46 +        NONE => []
    1.47 +      | SOME t => the_default [] (all_axioms_of lthy t)
    1.48      val goals = case some_locale
    1.49       of NONE => [(proto_goal, eval_terms)]
    1.50        | SOME locale =>
    1.51 -          (Logic.list_implies (assms_of locale, proto_goal), eval_terms) ::
    1.52 +          (Logic.list_implies (axioms_of locale, proto_goal), eval_terms) ::
    1.53            map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
    1.54            (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
    1.55 +    val _ = verbose_message lthy (Pretty.string_of
    1.56 +      (Pretty.big_list ("Checking goals: ") (map (Syntax.pretty_term lthy o fst) goals)))
    1.57    in
    1.58      test_terms lthy (time_limit, is_interactive) insts goals
    1.59    end