--- a/Nominal/Fv.thy	Tue Mar 02 14:51:40 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 02 15:10:47 2010 +0100
@@ -443,4 +443,13 @@
 1 *})
 done*)
 
+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

--- a/Nominal/Rsp.thy	Tue Mar 02 14:51:40 2010 +0100
+++ b/Nominal/Rsp.thy	Tue Mar 02 15:10:47 2010 +0100
@@ -175,4 +175,9 @@
 end
 *}
 
+ML {*
+fun build_bv_eqvt perms simps inducts (t, n) =
+  build_eqvts Binding.empty [t] [nth perms n] simps (nth inducts n)
+*}
+
 end