src/HOL/Tools/Function/mutual.ML
changeset 60321 42079156c5aa
parent 59859 f9d1442c70f3
child 60643 9173467ec5b6
equal deleted inserted replaced
60320:e7c0ca878120 60321:42079156c5aa
   248 fun mutual_cases_rule ctxt cases_rule n ST (MutualPart {i, cargTs = Ts, ...}) =
   248 fun mutual_cases_rule ctxt cases_rule n ST (MutualPart {i, cargTs = Ts, ...}) =
   249   let
   249   let
   250     val [P, x] =
   250     val [P, x] =
   251       Variable.variant_frees ctxt [] [("P", @{typ bool}), ("x", HOLogic.mk_tupleT Ts)]
   251       Variable.variant_frees ctxt [] [("P", @{typ bool}), ("x", HOLogic.mk_tupleT Ts)]
   252       |> map (Thm.cterm_of ctxt o Free);
   252       |> map (Thm.cterm_of ctxt o Free);
   253     val sumtree_inj = Drule.cterm_fun (Sum_Tree.mk_inj ST n i) x;
   253     val sumtree_inj = Thm.cterm_of ctxt (Sum_Tree.mk_inj ST n i (Thm.term_of x));
   254 
   254 
   255     fun prep_subgoal_tac i =
   255     fun prep_subgoal_tac i =
   256       REPEAT (eresolve_tac ctxt
   256       REPEAT (eresolve_tac ctxt
   257         @{thms Pair_inject Inl_inject [elim_format] Inr_inject [elim_format]} i)
   257         @{thms Pair_inject Inl_inject [elim_format] Inr_inject [elim_format]} i)
   258       THEN REPEAT (eresolve_tac ctxt
   258       THEN REPEAT (eresolve_tac ctxt