src/HOL/Tools/Quickcheck/quickcheck_common.ML
changeset 46312 518cc38a1a8c
parent 45923 473b744c23f2
child 46327 ecda23528833
equal deleted inserted replaced
46311:56fae81902ce 46312:518cc38a1a8c
   260 fun preprocess ctxt t =
   260 fun preprocess ctxt t =
   261   let
   261   let
   262     val thy = Proof_Context.theory_of ctxt
   262     val thy = Proof_Context.theory_of ctxt
   263     val dest = HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of
   263     val dest = HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of
   264     val rewrs = map (swap o dest) @{thms all_simps} @
   264     val rewrs = map (swap o dest) @{thms all_simps} @
   265       (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}])
   265       (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}, @{thm fun_eq_iff}])
   266     val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term thy t)
   266     val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term thy t)
   267     val (vs, body) = strip_all t'
   267     val (vs, body) = strip_all t'
   268     val vs' = Variable.variant_frees ctxt [t'] vs
   268     val vs' = Variable.variant_frees ctxt [t'] vs
   269   in
   269   in
   270     subst_bounds (map Free (rev vs'), body)
   270     subst_bounds (map Free (rev vs'), body)