src/Tools/quickcheck.ML
changeset 46343 6d9535e52915
parent 45765 cb6ddee6a463
child 46477 db693eb03a3f
equal deleted inserted replaced
46342:c59b8560eb48 46343:6d9535e52915
   322       | SOME locale => SOME locale;
   322       | SOME locale => SOME locale;
   323     val assms = if Config.get lthy no_assms then [] else case some_locale
   323     val assms = if Config.get lthy no_assms then [] else case some_locale
   324      of NONE => Assumption.all_assms_of lthy
   324      of NONE => Assumption.all_assms_of lthy
   325       | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);
   325       | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);
   326     val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
   326     val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
       
   327     fun assms_of locale = case fst (Locale.intros_of thy locale) of NONE => []
       
   328       | SOME th =>
       
   329           let
       
   330             val t = the_single (Assumption.all_assms_of (Locale.init locale thy))
       
   331             val (tyenv, tenv) =
       
   332               Pattern.match thy (concl_of th, term_of t) (Vartab.empty, Vartab.empty)
       
   333           in
       
   334             map (Envir.subst_term (tyenv, tenv)) (prems_of th)
       
   335           end
   327     val goals = case some_locale
   336     val goals = case some_locale
   328      of NONE => [(proto_goal, eval_terms)]
   337      of NONE => [(proto_goal, eval_terms)]
   329       | SOME locale =>
   338       | SOME locale =>
   330         map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
   339           (Logic.list_implies (assms_of locale, proto_goal), eval_terms) ::
       
   340           map (fn (_, phi) => (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
   331           (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
   341           (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale);
   332   in
   342   in
   333     test_terms lthy (time_limit, is_interactive) insts goals
   343     test_terms lthy (time_limit, is_interactive) insts goals
   334   end
   344   end
   335 
   345