# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267539047 -3600
# Node ID 80dabcaafc38418df4fb43a83a3974c9cf0951c0
# Parent  dc65319809cc460b4204f71b9493aaf91194ec47
Moving wrappers out of Lift.

diff -r dc65319809cc -r 80dabcaafc38 Nominal/Fv.thy
--- 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
diff -r dc65319809cc -r 80dabcaafc38 Nominal/Rsp.thy
--- 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