diff -r c7d4bd9e89e0 -r 23befefc6e73 Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Tue Jun 07 08:52:59 2011 +0100
+++ b/Nominal/nominal_function_core.ML	Tue Jun 07 10:40:06 2011 +0100
@@ -8,48 +8,6 @@
 *)
 
 
-structure Nominal_Function_Common =
-struct
-
-
-(* Configuration management *)
-datatype nominal_function_opt
-  = Sequential
-  | Default of string
-  | DomIntros
-  | No_Partials
-  | Invariant of string
-
-datatype nominal_function_config = NominalFunctionConfig of
- {sequential: bool,
-  default: string option,
-  domintros: bool,
-  partials: bool,
-  inv: string option}
-
-fun apply_opt Sequential (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
-    NominalFunctionConfig 
-      {sequential=true, default=default, domintros=domintros, partials=partials, inv=inv}
-  | apply_opt (Default d) (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
-    NominalFunctionConfig 
-      {sequential=sequential, default=SOME d, domintros=domintros, partials=partials, inv=inv}
-  | apply_opt DomIntros (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
-    NominalFunctionConfig 
-      {sequential=sequential, default=default, domintros=true, partials=partials, inv=inv}
-  | apply_opt No_Partials (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
-    NominalFunctionConfig 
-      {sequential=sequential, default=default, domintros=domintros, partials=false, inv=inv}
-  | apply_opt (Invariant s) (NominalFunctionConfig {sequential, default, domintros, partials, inv}) =
-    NominalFunctionConfig 
-      {sequential=sequential, default=default, domintros=domintros, partials=partials, inv = SOME s}
-
-val nominal_default_config =
-  NominalFunctionConfig { sequential=false, default=NONE,
-    domintros=false, partials=true, inv=NONE}
-
-end
-
-
 signature NOMINAL_FUNCTION_CORE =
 sig
   val trace: bool Unsynchronized.ref