src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
changeset 61424 c3658c18b7bc
parent 61268 abe08fb15a12
child 62354 fdd6989cc8a0
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -610,7 +610,7 @@
     1.4        | mk_tuple tTs = foldr1 mk_prod tTs
     1.5      fun mk_split_abs (T as Type (@{type_name Product_Type.prod}, [T1, T2])) t =
     1.6            absdummy T
     1.7 -            (HOLogic.split_const (T1, T2, @{typ bool}) $ (mk_split_abs T1 (mk_split_abs T2 t)))
     1.8 +            (HOLogic.case_prod_const (T1, T2, @{typ bool}) $ (mk_split_abs T1 (mk_split_abs T2 t)))
     1.9        | mk_split_abs T t = absdummy T t
    1.10      val args = rev (fst (fold_map mk_bounds (rev (binder_types T)) 0))
    1.11      val (inargs, outargs) = split_mode mode args
    1.12 @@ -1023,7 +1023,7 @@
    1.13  
    1.14  (* Definition of executable functions and their intro and elim rules *)
    1.15  
    1.16 -fun strip_split_abs (Const (@{const_name uncurry}, _) $ t) = strip_split_abs t
    1.17 +fun strip_split_abs (Const (@{const_name case_prod}, _) $ t) = strip_split_abs t
    1.18    | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
    1.19    | strip_split_abs t = t
    1.20  
    1.21 @@ -1086,7 +1086,7 @@
    1.22      val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
    1.23      val simprules =
    1.24        [defthm, @{thm eval_pred},
    1.25 -        @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]
    1.26 +        @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm prod.collapse}]
    1.27      val unfolddef_tac =
    1.28        Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simprules) 1
    1.29      val introthm = Goal.prove ctxt
    1.30 @@ -1748,7 +1748,7 @@
    1.31        (case t_compr of
    1.32          (Const (@{const_name Collect}, _) $ t) => t
    1.33        | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr))
    1.34 -    val (body, Ts, fp) = HOLogic.strip_psplits inner_t;
    1.35 +    val (body, Ts, fp) = HOLogic.strip_ptupleabs inner_t;
    1.36      val output_names = Name.variant_list (Term.add_free_names body [])
    1.37        (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
    1.38      val output_frees = map2 (curry Free) output_names (rev Ts)