210      DT ctxt "E" (WEAK_LAMBDA_RES_TAC ctxt),

   210      DT ctxt "E" (WEAK_LAMBDA_RES_TAC ctxt),

   211      DT ctxt "F" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]

   211      DT ctxt "F" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]

   212 *}

   212 *}

   213 

   213 

   214 ML {* 

   214 ML {* 

   216   |> Syntax.check_term @{context}

   216   |> Syntax.check_term @{context}

   217 *}

   217 *}

   218 

   218 

   219 

   219 

   220 ML {* val my_goal = cterm_of @{theory} (mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm)) *}

   220 ML {* val my_goal = cterm_of @{theory} (mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm)) *}

   224 apply(tactic {* ObjectLogic.full_atomize_tac 1 *})

   224 apply(tactic {* ObjectLogic.full_atomize_tac 1 *})

   225 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})

   225 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})

   226 done

   226 done

   227 

   227 

   228 ML {*

   228 ML {*

   230 |> Syntax.string_of_term @{context}

   230 |> Syntax.string_of_term @{context}

   231 |> writeln

   231 |> writeln

   232 *}

   232 *}

   233 

   233 

   234 *)

   234 *)