Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Quickcheck/abstract_generators.ML
changeset 80634 a90ab1ea6458
parent 67149 e61557884799 
--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML	Sun Aug 04 13:14:33 2024 +0200
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML	Sun Aug 04 13:24:54 2024 +0200
@@ -33,7 +33,7 @@
     val opt_pred = Option.map (prep_term ctxt) opt_pred_raw
     val constrs = map (prep_term ctxt) constrs_raw
     val _ = check_constrs ctxt tyco constrs
-    val vs = map dest_TFree (snd (dest_Type (body_type (fastype_of (hd constrs)))))
+    val vs = map dest_TFree (dest_Type_args (body_type (fastype_of (hd constrs))))
     val name = Long_Name.base_name tyco
     fun mk_dconstrs (Const (s, T)) =
           (s, map (Old_Datatype_Aux.dtyp_of_typ [(tyco, vs)]) (binder_types T))
@@ -61,7 +61,7 @@
 
 val quickcheck_generator_cmd =
   gen_quickcheck_generator
-    ((#1 o dest_Type) oo Proof_Context.read_type_name {proper = true, strict = true})
+    (dest_Type_name oo Proof_Context.read_type_name {proper = true, strict = true})
     Syntax.read_term
 
 val _ =
isabelle