--- a/Nominal/Tacs.thy	Fri Mar 26 10:55:13 2010 +0100
+++ b/Nominal/Tacs.thy	Fri Mar 26 16:20:39 2010 +0100
@@ -125,5 +125,46 @@
 end
 *}
 
+ML {*
+fun repeat_mp thm = repeat_mp (mp OF [thm]) handle THM _ => thm
+*}
+
+(* Introduces an implication and immediately eliminates it by cases *)
+ML {*
+fun imp_elim_tac case_rules =
+  Subgoal.FOCUS (fn {concl, context, ...} =>
+    case term_of concl of
+      _ $ (_ $ asm $ _) =>
+        let
+          fun filter_fn case_rule = (
+            case Logic.strip_assums_hyp (prop_of case_rule) of
+              ((_ $ asmc) :: _) =>
+                let
+                  val thy = ProofContext.theory_of context
+                in
+                  Pattern.matches thy (asmc, asm)
+                end
+            | _ => false)
+          val matching_rules = filter filter_fn case_rules
+        in
+         (rtac impI THEN' rotate_tac (~1) THEN' eresolve_tac matching_rules) 1
+        end
+    | _ => no_tac)
+*}
+
+ML {*
+fun is_ex (Const ("Ex", _) $ Abs _) = true
+  | is_ex _ = false;
+*}
+
+ML {*
+fun dtyp_no_of_typ _ (TFree (n, _)) = error "dtyp_no_of_typ: Illegal free"
+  | dtyp_no_of_typ _ (TVar _) = error "dtyp_no_of_typ: Illegal schematic"
+  | dtyp_no_of_typ dts (Type (tname, Ts)) =
+      case try (find_index (curry op = tname o fst)) dts of
+        NONE => error "dtyp_no_of_typ: Illegal recursion"
+      | SOME i => i
+*}
+
 end