src/HOL/Tools/Predicate_Compile/code_prolog.ML
changeset 61424 c3658c18b7bc
parent 61268 abe08fb15a12
child 62519 a564458f94db
     1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -956,7 +956,7 @@
     1.4        (case t_compr of
     1.5          (Const (@{const_name Collect}, _) $ t) => t
     1.6        | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr))
     1.7 -    val (body, Ts, fp) = HOLogic.strip_psplits split
     1.8 +    val (body, Ts, fp) = HOLogic.strip_ptupleabs split
     1.9      val output_names = Name.variant_list (Term.add_free_names body [])
    1.10        (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
    1.11      val output_frees = rev (map2 (curry Free) output_names Ts)