# HG changeset patch
# User wenzelm
# Date 1010768865 -3600
# Node ID 0451211bf4a08f4d3016476eba618d4a805881b6
# Parent  5af701433ea167a177f6185755919e04088b83f7
removed obsolete isamode.ML;

diff -r 5af701433ea1 -r 0451211bf4a0 src/Pure/Interface/ROOT.ML
--- a/src/Pure/Interface/ROOT.ML	Fri Jan 11 18:07:30 2002 +0100
+++ b/src/Pure/Interface/ROOT.ML	Fri Jan 11 18:07:45 2002 +0100
@@ -4,5 +4,4 @@
 Specific support for user-interfaces.
 *)
 
-use "isamode.ML";
 use "proof_general.ML";
diff -r 5af701433ea1 -r 0451211bf4a0 src/Pure/Interface/isamode.ML
--- a/src/Pure/Interface/isamode.ML	Fri Jan 11 18:07:30 2002 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-(*  Title:      Pure/Interface/isamode.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Configuration for David Aspinall's Isamode.
-*)
-
-signature ISAMODE =
-sig
-  val setup: (theory -> theory) list
-  val init: bool -> unit
-end;
-
-structure Isamode: ISAMODE =
-struct
-
-(** compile-time theory setup **)
-
-(* token translations *)
-
-val isamodeN = "Isamode";
-
-local
-
-val end_tag = "\^A0";
-val tclass_tag = "\^A1";
-val tfree_tag = "\^A2";
-val tvar_tag = "\^A3";
-val free_tag = "\^A4";
-val bound_tag = "\^A5";
-val var_tag = "\^A6";
-
-fun tagit p x = (p ^ x ^ end_tag, real (size x));
-
-in
-
-val isamode_trans =
- Syntax.tokentrans_mode isamodeN
-  [("class", tagit tclass_tag),
-   ("tfree", tagit tfree_tag),
-   ("tvar", tagit tvar_tag),
-   ("free", tagit free_tag),
-   ("bound", tagit bound_tag),
-   ("var", tagit var_tag)];
-
-end;
-
-
-(* setup *)
-
-val setup = [Theory.add_tokentrfuns isamode_trans];
-
-
-
-(** run-time initialization **)
-
-fun init isamode =
-  if isamode then print_mode := isamodeN :: ! print_mode else ();
-
-
-end;
diff -r 5af701433ea1 -r 0451211bf4a0 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Fri Jan 11 18:07:30 2002 +0100
+++ b/src/Pure/IsaMakefile	Fri Jan 11 18:07:45 2002 +0100
@@ -28,11 +28,11 @@
   General/name_space.ML General/object.ML General/path.ML		\
   General/position.ML General/pretty.ML General/scan.ML General/seq.ML	\
   General/source.ML General/symbol.ML General/table.ML General/url.ML	\
-  General/xml.ML Interface/ROOT.ML Interface/isamode.ML			\
-  Interface/proof_general.ML Isar/ROOT.ML Isar/antiquote.ML 		\
-  Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML	\
-  Isar/comment.ML Isar/context_rules.ML Isar/induct_attrib.ML 		\
-  Isar/isar.ML Isar/isar_cmd.ML Isar/isar_output.ML Isar/isar_syn.ML	\
+  General/xml.ML Interface/ROOT.ML Interface/proof_general.ML		\
+  Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML		\
+  Isar/auto_bind.ML Isar/calculation.ML Isar/comment.ML			\
+  Isar/context_rules.ML Isar/induct_attrib.ML Isar/isar.ML		\
+  Isar/isar_cmd.ML Isar/isar_output.ML Isar/isar_syn.ML			\
   Isar/isar_thy.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML	\
   Isar/object_logic.ML Isar/obtain.ML Isar/outer_lex.ML			\
   Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML		\
diff -r 5af701433ea1 -r 0451211bf4a0 src/Pure/pure.ML
--- a/src/Pure/pure.ML	Fri Jan 11 18:07:30 2002 +0100
+++ b/src/Pure/pure.ML	Fri Jan 11 18:07:45 2002 +0100
@@ -21,7 +21,6 @@
     AxClass.setup @
     Latex.setup @
     Present.setup @
-    Isamode.setup @
     ProofGeneral.setup @
     Codegen.setup @
     Goals.setup;