128 ML {*

   129 fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm

   130 *}

   131 

   132 (* Introduces an implication and immediately eliminates it by cases *)

   133 ML {*

   134 fun imp_elim_tac case_rules =

   135   Subgoal.FOCUS (fn {concl, context, ...} =>

   136     case term_of concl of

   137       _ $ (_ $ asm $ _) =>

   138         let

   139           fun filter_fn case_rule = (

   140             case Logic.strip_assums_hyp (prop_of case_rule) of

   141               ((_ $ asmc) :: _) =>

   142                 let

   143                   val thy = ProofContext.theory_of context

   144                 in

   145                   Pattern.matches thy (asmc, asm)

   146                 end

   147             | _ => false)

   148           val matching_rules = filter filter_fn case_rules

   149         in

   150          (rtac impI THEN' rotate_tac (~1) THEN' eresolve_tac matching_rules) 1

   151         end

   152     | _ => no_tac)

   153 *}

   154 

   155 ML {*

   156 fun is_ex (Const ("Ex", _) $ Abs _) = true

   157   | is_ex _ = false;

   158 *}

   159 

   160 ML {*

   161 fun dtyp_no_of_typ _ (TFree (n, _)) = error "dtyp_no_of_typ: Illegal free"

   162   | dtyp_no_of_typ _ (TVar _) = error "dtyp_no_of_typ: Illegal schematic"

   163   | dtyp_no_of_typ dts (Type (tname, Ts)) =

   164       case try (find_index (curry op = tname o fst)) dts of

   165         NONE => error "dtyp_no_of_typ: Illegal recursion"

   166       | SOME i => i

   167 *}

   168