# HG changeset patch
# User haftmann
# Date 1281532171 -7200
# Node ID 2dfd8b7b8274fd72b3798afb60f9aeb68785de9a
# Parent  dc67291d590b2a6b390607d2014c222b142d44f4
stripped signature

diff -r dc67291d590b -r 2dfd8b7b8274 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Wed Aug 11 15:09:30 2010 +0200
+++ b/src/Pure/Isar/class_target.ML	Wed Aug 11 15:09:31 2010 +0200
@@ -7,31 +7,17 @@
 signature CLASS_TARGET =
 sig
   (*classes*)
-  val register: class -> class list -> ((string * typ) * (string * typ)) list
-    -> sort -> morphism -> morphism -> thm option -> thm option -> thm
-    -> theory -> theory
-
   val is_class: theory -> class -> bool
-  val base_sort: theory -> class -> sort
-  val rules: theory -> class -> thm option * thm
   val these_params: theory -> sort -> (string * (class * (string * typ))) list
-  val these_defs: theory -> sort -> thm list
-  val these_operations: theory -> sort
-    -> (string * (class * (typ * term))) list
   val print_classes: theory -> unit
 
-  val begin: class list -> sort -> Proof.context -> Proof.context
   val init: class -> theory -> Proof.context
   val declare: class -> (binding * mixfix) * (term list * term) -> theory -> theory
   val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory
   val class_prefix: string -> string
   val refresh_syntax: class -> Proof.context -> Proof.context
-  val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
 
   (*instances*)
-  val init_instantiation: string list * (string * sort) list * sort
-    -> theory -> Proof.context
-  val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
   val instantiation_instance: (local_theory -> local_theory)
     -> local_theory -> Proof.state
   val prove_instantiation_instance: (Proof.context -> tactic)
@@ -40,19 +26,14 @@
     -> local_theory -> theory
   val prove_instantiation_exit_result: (morphism -> 'a -> 'b)
     -> (Proof.context -> 'b -> tactic) -> 'a -> local_theory -> 'b * theory
-  val conclude_instantiation: local_theory -> local_theory
-  val instantiation_param: local_theory -> binding -> string option
-  val confirm_declaration: binding -> local_theory -> local_theory
-  val pretty_instantiation: local_theory -> Pretty.T
   val read_multi_arity: theory -> xstring list * xstring list * xstring
     -> string list * (string * sort) list * sort
   val type_name: string -> string
   val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
   val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
+  val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
 
   (*subclasses*)
-  val register_subclass: class * class -> morphism option -> Element.witness option
-    -> morphism -> theory -> theory
   val classrel: class * class -> theory -> Proof.state
   val classrel_cmd: xstring * xstring -> theory -> Proof.state
 
@@ -61,7 +42,24 @@
   val default_intro_tac: Proof.context -> thm list -> tactic
 end;
 
-structure Class_Target : CLASS_TARGET =
+signature PRIVATE_CLASS_TARGET =
+sig
+  include CLASS_TARGET
+  val register: class -> class list -> ((string * typ) * (string * typ)) list
+    -> sort -> morphism -> morphism -> thm option -> thm option -> thm
+    -> theory -> theory
+  val register_subclass: class * class -> morphism option -> Element.witness option
+    -> morphism -> theory -> theory
+  val base_sort: theory -> class -> sort
+  val rules: theory -> class -> thm option * thm
+  val these_defs: theory -> sort -> thm list
+  val these_operations: theory -> sort
+    -> (string * (class * (typ * term))) list
+  val begin: class list -> sort -> Proof.context -> Proof.context
+  val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
+end;
+
+structure Class_Target: PRIVATE_CLASS_TARGET =
 struct
 
 (** class data **)
diff -r dc67291d590b -r 2dfd8b7b8274 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Wed Aug 11 15:09:30 2010 +0200
+++ b/src/Pure/Isar/overloading.ML	Wed Aug 11 15:09:31 2010 +0200
@@ -6,14 +6,6 @@
 
 signature OVERLOADING =
 sig
-  val init: (string * (string * typ) * bool) list -> theory -> Proof.context
-  val conclude: local_theory -> local_theory
-  val declare: string * typ -> theory -> term * theory
-  val confirm: binding -> local_theory -> local_theory
-  val define: bool -> binding -> string * term -> theory -> thm * theory
-  val operation: Proof.context -> binding -> (string * bool) option
-  val pretty: Proof.context -> Pretty.T
-
   type improvable_syntax
   val add_improvable_syntax: Proof.context -> Proof.context
   val map_improvable_syntax: (improvable_syntax -> improvable_syntax)