# HG changeset patch
# User wenzelm
# Date 1262643635 -3600
# Node ID 2ba492b8b6e89e961754d950645b081cc926ff9f
# Parent  e936d3c35ce0024e84d71d6538f65803ff1e9c2c
discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);

diff -r e936d3c35ce0 -r 2ba492b8b6e8 NEWS
--- a/NEWS	Mon Jan 04 22:43:07 2010 +0100
+++ b/NEWS	Mon Jan 04 23:20:35 2010 +0100
@@ -47,6 +47,11 @@
 * Subgoal.FOCUS (and variants): resulting goal state is normalized as
 usual for resolution.  Rare INCOMPATIBILITY.
 
+* Discontinued old TheoryDataFun with its copy/init operation -- data
+needs to be pure.  Functor Theory_Data_PP retains the traditional
+Pretty.pp argument to merge, which is absent in the standard
+Theory_Data version.
+
 
 *** System ***
 
diff -r e936d3c35ce0 -r 2ba492b8b6e8 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Mon Jan 04 22:43:07 2010 +0100
+++ b/src/Pure/axclass.ML	Mon Jan 04 23:20:35 2010 +0100
@@ -114,7 +114,7 @@
 
 (* setup data *)
 
-structure AxClassData = TheoryDataFun
+structure AxClassData = Theory_Data_PP
 (
   type T = axclasses * (instances * inst_params);
   val empty = ((Symtab.empty, []), (([], Symtab.empty), (Symtab.empty, Symtab.empty)));
diff -r e936d3c35ce0 -r 2ba492b8b6e8 src/Pure/context.ML
--- a/src/Pure/context.ML	Mon Jan 04 22:43:07 2010 +0100
+++ b/src/Pure/context.ML	Mon Jan 04 23:20:35 2010 +0100
@@ -574,7 +574,7 @@
 
 (** theory data **)
 
-signature OLD_THEORY_DATA_ARGS =
+signature THEORY_DATA_PP_ARGS =
 sig
   type T
   val empty: T
@@ -582,6 +582,14 @@
   val merge: Pretty.pp -> T * T -> T
 end;
 
+signature THEORY_DATA_ARGS =
+sig
+  type T
+  val empty: T
+  val extend: T -> T
+  val merge: T * T -> T
+end;
+
 signature THEORY_DATA =
 sig
   type T
@@ -590,7 +598,7 @@
   val map: (T -> T) -> theory -> theory
 end;
 
-functor TheoryDataFun(Data: OLD_THEORY_DATA_ARGS): THEORY_DATA =
+functor Theory_Data_PP(Data: THEORY_DATA_PP_ARGS): THEORY_DATA =
 struct
 
 type T = Data.T;
@@ -607,28 +615,14 @@
 
 end;
 
-signature THEORY_DATA_ARGS =
-sig
-  type T
-  val empty: T
-  val extend: T -> T
-  val merge: T * T -> T
-end;
-
 functor Theory_Data(Data: THEORY_DATA_ARGS): THEORY_DATA =
-struct
-
-structure Result = TheoryDataFun
-(
-  type T = Data.T;
-  val empty = Data.empty;
-  val extend = Data.extend;
-  fun merge _ = Data.merge;
-);
-
-open Result;
-
-end;
+  Theory_Data_PP
+  (
+    type T = Data.T;
+    val empty = Data.empty;
+    val extend = Data.extend;
+    fun merge _ = Data.merge;
+  );
 
 
 
diff -r e936d3c35ce0 -r 2ba492b8b6e8 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Jan 04 22:43:07 2010 +0100
+++ b/src/Pure/sign.ML	Mon Jan 04 23:20:35 2010 +0100
@@ -148,7 +148,7 @@
 fun make_sign (naming, syn, tsig, consts) =
   Sign {naming = naming, syn = syn, tsig = tsig, consts = consts};
 
-structure SignData = TheoryDataFun
+structure SignData = Theory_Data_PP
 (
   type T = sign;
   fun extend (Sign {syn, tsig, consts, ...}) =
diff -r e936d3c35ce0 -r 2ba492b8b6e8 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Mon Jan 04 22:43:07 2010 +0100
+++ b/src/Pure/theory.ML	Mon Jan 04 23:20:35 2010 +0100
@@ -86,7 +86,7 @@
 
 fun make_thy (axioms, defs, wrappers) = Thy {axioms = axioms, defs = defs, wrappers = wrappers};
 
-structure ThyData = TheoryDataFun
+structure ThyData = Theory_Data_PP
 (
   type T = thy;
   val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table;