1091 apply (simp only: FUN_REL.simps)

  1092 apply (rule allI)

  1093 apply (rule allI)

  1094 apply (rule impI)

  1095 ML_prf {*

  1096   val concl = (#concl o fst) (Subgoal.focus @{context} 1 (Isar.goal ()));

  1097   val pat = Drule.strip_imp_concl (cprop_of @{thm RES_FORALL_RSP});

  1098   val ((_,p),(_,c)) = (Thm.dest_comb pat, Thm.dest_comb concl);

  1099   val ((_,p),(_,c)) = (Thm.dest_comb p, Thm.dest_comb c);

  1100 *}

  1101 ML_prf {*

  1102   val ((_,pn),(_,cn)) = (Thm.dest_comb p, Thm.dest_comb c);

  1103   val (pnm, cnm) = (@{cpat "?a"}, @{cterm "b::('a List.list \<Rightarrow> bool)"});

  1104   val (pp, cc) = (term_of pn, term_of cn);

  1105   val (ppt, cct) = (type_of pp, type_of cc);

  1106   val (ppm, ccm) = (term_of pnm, term_of cnm);

  1107   val i = Pattern.first_order_match @{theory} (ppm, ccm) (Vartab.empty, Vartab.empty);

  1108   val (ppmt, ccmt) = (type_of ppm, type_of ccm);

  1109   val ii = Sign.typ_match @{theory} (ppmt, cct) (Vartab.empty);

  1110   val ii = Sign.typ_match @{theory} (ppt, cct) (Vartab.empty);

  1111 *}

  1112 .

  1113   val pat = Drule.strip_imp_concl (cprop_of thm)

  1114   val insts = Thm.match (pat, concl)

  1115 

  1116 apply (tactic {* instantiate_tac @{thm RES_FORALL_RSP} @{context} 1 *})

  1117 thm RES_FORALL_RSP

  1118 apply (rule_tac RES_FORALL_RSP)

  1119