# HG changeset patch
# User wenzelm
# Date 1232576504 -3600
# Node ID fedb8be05f2401f62721a7ecc92d683efc1d078a
# Parent  f2924219125ecd17982cbb48680f9740a12a05e3
removed Ids;

diff -r f2924219125e -r fedb8be05f24 src/Pure/General/ROOT.ML
--- a/src/Pure/General/ROOT.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/ROOT.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/ROOT.ML
-    ID:         $Id$
 
 Library of general tools.
 *)
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/alist.ML
--- a/src/Pure/General/alist.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/alist.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/alist.ML
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
 Association lists -- lists of (key, value) pairs.
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/balanced_tree.ML
--- a/src/Pure/General/balanced_tree.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/balanced_tree.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/balanced_tree.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson and Makarius
 
 Balanced binary trees.
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/basics.ML
--- a/src/Pure/General/basics.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/basics.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/basics.ML
-    ID:         $Id$
     Author:     Florian Haftmann and Makarius, TU Muenchen
 
 Fundamental concepts.
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/file.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/file.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 File system operations.
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/graph.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/graph.ML
-    ID:         $Id$
     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
 
 Directed graphs.
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/heap.ML
--- a/src/Pure/General/heap.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/heap.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,6 +1,5 @@
 (*  Title:      Pure/General/heap.ML
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
+    Author:     Lawrence C Paulson and Markus Wenzel
 
 Heaps over linearly ordered types.  See also Chris Okasaki: "Purely
 Functional Data Structures" (Chapter 3), Cambridge University Press,
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/integer.ML
--- a/src/Pure/General/integer.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/integer.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/integer.ML
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
 Unbounded integers.
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/ord_list.ML
--- a/src/Pure/General/ord_list.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/ord_list.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/ord_list.ML
-    ID:         $Id$
     Author:     Makarius
 
 Ordered lists without duplicates -- a light-weight representation of
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/output.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/output.ML
-    ID:         $Id$
     Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
 
 Output channels and timing messages.
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/path.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/path.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Abstract algebra of file paths (external encoding in Unix style).
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/pretty.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/pretty.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Markus Wenzel, TU Munich
 
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/print_mode.ML
--- a/src/Pure/General/print_mode.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/print_mode.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/print_mode.ML
-    ID:         $Id$
     Author:     Makarius
 
 Generic print mode as thread-local value derived from global template;
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/properties.ML
--- a/src/Pure/General/properties.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/properties.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/properties.ML
-    ID:         $Id$
     Author:     Makarius
 
 Property lists.
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/queue.ML
--- a/src/Pure/General/queue.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/queue.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/queue.ML
-    ID:         $Id$
     Author:     Makarius
 
 Efficient queues.
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/scan.ML
--- a/src/Pure/General/scan.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/scan.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/scan.ML
-    ID:         $Id$
     Author:     Markus Wenzel and Tobias Nipkow, TU Muenchen
 
 Generic scanners (for potentially infinite input).
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/secure.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/secure.ML
-    ID:         $Id$
     Author:     Makarius
 
 Secure critical operations.
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/seq.ML
--- a/src/Pure/General/seq.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/seq.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/seq.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Markus Wenzel, TU Munich
 
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/source.ML
--- a/src/Pure/General/source.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/source.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/source.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Coalgebraic data sources -- efficient purely functional input streams.
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/stack.ML
--- a/src/Pure/General/stack.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/stack.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/stack.ML
-    ID:         $Id$
     Author:     Makarius
 
 Non-empty stacks.
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/symbol.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/symbol.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Generalized characters with infinitely many named symbols.
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/symbol_pos.ML
--- a/src/Pure/General/symbol_pos.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/symbol_pos.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/symbol_pos.ML
-    ID:         $Id$
     Author:     Makarius
 
 Symbols with explicit position information.
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/table.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/table.ML
-    ID:         $Id$
     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
 
 Generic tables.  Efficient purely functional implementation using
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/url.ML
--- a/src/Pure/General/url.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/url.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/url.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Basic URLs, see RFC 1738 and RFC 2396.
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/xml.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/xml.ML
-    ID:         $Id$
     Author:     David Aspinall, Stefan Berghofer and Markus Wenzel
 
 Basic support for XML.
diff -r f2924219125e -r fedb8be05f24 src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/General/yxml.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/General/yxml.ML
-    ID:         $Id$
     Author:     Makarius
 
 Efficient text representation of XML trees using extra characters X
diff -r f2924219125e -r fedb8be05f24 src/Pure/Isar/antiquote.ML
--- a/src/Pure/Isar/antiquote.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/antiquote.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/antiquote.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Text with antiquotations of inner items (terms, types etc.).
diff -r f2924219125e -r fedb8be05f24 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/args.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/args.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Parsing with implicit value assigment.  Concrete argument syntax of
diff -r f2924219125e -r fedb8be05f24 src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/auto_bind.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/auto_bind.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Automatic bindings of Isar text elements.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/calculation.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/calculation.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Generic calculational proofs.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/context_rules.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/context_rules.ML
-    ID:         $Id$
     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
 
 Declarations of intro/elim/dest rules in Pure (see also
diff -r f2924219125e -r fedb8be05f24 src/Pure/Isar/local_syntax.ML
--- a/src/Pure/Isar/local_syntax.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/local_syntax.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/local_syntax.ML
-    ID:         $Id$
     Author:     Makarius
 
 Local syntax depending on theory syntax.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Isar/net_rules.ML
--- a/src/Pure/Isar/net_rules.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/net_rules.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/net_rules.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Efficient storage of rules: preserves order, prefers later entries.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/object_logic.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/object_logic.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Specifics about common object-logics.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/outer_lex.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/outer_lex.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Outer lexical syntax for Isabelle/Isar.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/overloading.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/overloading.ML
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
 Overloaded definitions without any discipline.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/proof_context.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 The key concept of Isar proof contexts: elevates primitive local
diff -r f2924219125e -r fedb8be05f24 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/proof_display.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/proof_display.ML
-    ID:         $Id$
     Author:     Makarius
 
 Printing of theorems, goals, results etc.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Isar/proof_node.ML
--- a/src/Pure/Isar/proof_node.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/proof_node.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/proof_node.ML
-    ID:         $Id$
     Author:     Makarius
 
 Proof nodes with linear position and backtracking.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/rule_insts.ML
-    ID:         $Id$
     Author:     Makarius
 
 Rule instantiations -- operations within a rule/subgoal context.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/skip_proof.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/skip_proof.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Skipping proofs -- quick_and_dirty mode.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/specification.ML
-    ID:         $Id$
     Author:     Makarius
 
 Derived local theory specifications --- with type-inference and
diff -r f2924219125e -r fedb8be05f24 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ML/ml_antiquote.ML
-    ID:         $Id$
     Author:     Makarius
 
 Common ML antiquotations.
diff -r f2924219125e -r fedb8be05f24 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ML/ml_context.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ML/ml_context.ML
-    ID:         $Id$
     Author:     Makarius
 
 ML context and antiquotations.
diff -r f2924219125e -r fedb8be05f24 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ML/ml_lex.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ML/ml_lex.ML
-    ID:         $Id$
     Author:     Makarius
 
 Lexical syntax for SML.
diff -r f2924219125e -r fedb8be05f24 src/Pure/ML/ml_parse.ML
--- a/src/Pure/ML/ml_parse.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ML/ml_parse.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ML/ml_parse.ML
-    ID:         $Id$
     Author:     Makarius
 
 Minimal parsing for SML -- fixing integer numerals.
diff -r f2924219125e -r fedb8be05f24 src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ML/ml_syntax.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ML/ml_syntax.ML
-    ID:         $Id$
     Author:     Makarius
 
 Basic ML syntax operations.
diff -r f2924219125e -r fedb8be05f24 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ML/ml_thms.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ML/ml_thms.ML
-    ID:         $Id$
     Author:     Makarius
 
 Isar theorem values within ML.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Proof/proof_syntax.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Function for parsing and printing proof terms.
diff -r f2924219125e -r fedb8be05f24 src/Pure/ProofGeneral/ROOT.ML
--- a/src/Pure/ProofGeneral/ROOT.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/ROOT.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ProofGeneral/ROOT.ML
-    ID:         $Id$
     Author:     David Aspinall
 
 Proof General interface for Isabelle, both the traditional Emacs version,
diff -r f2924219125e -r fedb8be05f24 src/Pure/ProofGeneral/pgip.ML
--- a/src/Pure/ProofGeneral/pgip.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ProofGeneral/pgip.ML
-    ID:         $Id$
     Author:     David Aspinall
 
 Prover-side PGIP abstraction.  
diff -r f2924219125e -r fedb8be05f24 src/Pure/ProofGeneral/pgip_input.ML
--- a/src/Pure/ProofGeneral/pgip_input.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_input.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ProofGeneral/pgip_input.ML
-    ID:         $Id$
     Author:     David Aspinall
 
 PGIP abstraction: input commands.
diff -r f2924219125e -r fedb8be05f24 src/Pure/ProofGeneral/pgip_isabelle.ML
--- a/src/Pure/ProofGeneral/pgip_isabelle.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ProofGeneral/pgip_isabelle.ML
-    ID:         $Id$
     Author:     David Aspinall
 
 Prover-side PGIP abstraction: Isabelle configuration and mapping to Isabelle types.
diff -r f2924219125e -r fedb8be05f24 src/Pure/ProofGeneral/pgip_markup.ML
--- a/src/Pure/ProofGeneral/pgip_markup.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_markup.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ProofGeneral/pgip_markup.ML
-    ID:         $Id$
     Author:     David Aspinall
 
 PGIP abstraction: document markup for proof scripts (in progress).
diff -r f2924219125e -r fedb8be05f24 src/Pure/ProofGeneral/pgip_output.ML
--- a/src/Pure/ProofGeneral/pgip_output.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_output.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ProofGeneral/pgip_output.ML
-    ID:         $Id$
     Author:     David Aspinall
 
 PGIP abstraction: output commands.
diff -r f2924219125e -r fedb8be05f24 src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ProofGeneral/pgip_parser.ML
-    ID:         $Id$
     Author:     David Aspinall and Makarius
 
 Parsing theory sources without execution (via keyword classification).
diff -r f2924219125e -r fedb8be05f24 src/Pure/ProofGeneral/pgip_tests.ML
--- a/src/Pure/ProofGeneral/pgip_tests.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_tests.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ProofGeneral/pgip_tests.ML
-    ID:         $Id$
     Author:     David Aspinall
 
 A test suite for the PGIP abstraction code (in progress).
diff -r f2924219125e -r fedb8be05f24 src/Pure/ProofGeneral/pgip_types.ML
--- a/src/Pure/ProofGeneral/pgip_types.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_types.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ProofGeneral/pgip_types.ML
-    ID:         $Id$
     Author:     David Aspinall
 
 PGIP abstraction: types and conversions.
diff -r f2924219125e -r fedb8be05f24 src/Pure/ProofGeneral/pgml.ML
--- a/src/Pure/ProofGeneral/pgml.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/pgml.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ProofGeneral/pgml.ML
-    ID:         $Id$
     Author:     David Aspinall
 
 PGIP abstraction: PGML
diff -r f2924219125e -r fedb8be05f24 src/Pure/ProofGeneral/proof_general_keywords.ML
--- a/src/Pure/ProofGeneral/proof_general_keywords.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_keywords.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ProofGeneral/proof_general_keywords.ML
-    ID:         $Id$
     Author:     Makarius
 
 Dummy session with outer syntax keyword initialization.
diff -r f2924219125e -r fedb8be05f24 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/ProofGeneral/proof_general_pgip.ML
-    ID:         $Id$
     Author:     David Aspinall and Markus Wenzel
 
 Isabelle configuration for Proof General using PGIP protocol.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Pure.thy	Wed Jan 21 23:21:44 2009 +0100
@@ -1,6 +1,3 @@
-(*  Title:      Pure/Pure.thy
-    ID:         $Id$
-*)
 
 section {* Further content for the Pure theory *}
 
diff -r f2924219125e -r fedb8be05f24 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Thy/html.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Thy/html.ML
-    ID:         $Id$
     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
 
 HTML presentation elements.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Thy/latex.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Thy/latex.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 LaTeX presentation elements -- based on outer lexical syntax.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Thy/present.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Thy/present.ML
-    ID:         $Id$
     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
 
 Theory presentation: HTML, graph files, (PDF)LaTeX documents.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Thy/term_style.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Thy/term_style.ML
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
 Styles for terms, to use with the "term_style" and "thm_style"
diff -r f2924219125e -r fedb8be05f24 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Thy/thm_deps.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Thy/thm_deps.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Visualize dependencies of theorems.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Thy/thy_header.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Thy/thy_header.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Theory headers -- independent of outer syntax.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Thy/thy_output.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Theory document output.
diff -r f2924219125e -r fedb8be05f24 src/Pure/Tools/xml_syntax.ML
--- a/src/Pure/Tools/xml_syntax.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/Tools/xml_syntax.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Tools/xml_syntax.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 
 Input and output of types, terms, and proofs in XML format.
diff -r f2924219125e -r fedb8be05f24 src/Pure/config.ML
--- a/src/Pure/config.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/config.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/config.ML
-    ID:         $Id$
     Author:     Makarius
 
 Configuration options as values within the local context.
diff -r f2924219125e -r fedb8be05f24 src/Pure/conjunction.ML
--- a/src/Pure/conjunction.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/conjunction.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/conjunction.ML
-    ID:         $Id$
     Author:     Makarius
 
 Meta-level conjunction.
diff -r f2924219125e -r fedb8be05f24 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/consts.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/consts.ML
-    ID:         $Id$
     Author:     Makarius
 
 Polymorphic constants: declarations, abbreviations, additional type
diff -r f2924219125e -r fedb8be05f24 src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/context_position.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/context_position.ML
-    ID:         $Id$
     Author:     Makarius
 
 Context position visibility flag.
diff -r f2924219125e -r fedb8be05f24 src/Pure/conv.ML
--- a/src/Pure/conv.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/conv.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/conv.ML
-    ID:         $Id$
     Author:     Amine Chaieb and Makarius
 
 Conversions: primitive equality reasoning.
diff -r f2924219125e -r fedb8be05f24 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/defs.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/defs.ML
-    ID:         $Id$
     Author:     Makarius
 
 Global well-formedness checks for constant definitions.  Covers plain
diff -r f2924219125e -r fedb8be05f24 src/Pure/display.ML
--- a/src/Pure/display.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/display.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/display.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
diff -r f2924219125e -r fedb8be05f24 src/Pure/interpretation.ML
--- a/src/Pure/interpretation.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/interpretation.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/interpretation.ML
-    ID:         $Id$
     Author:     Florian Haftmann and Makarius
 
 Generic interpretation of theory data.
diff -r f2924219125e -r fedb8be05f24 src/Pure/net.ML
--- a/src/Pure/net.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/net.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/net.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
diff -r f2924219125e -r fedb8be05f24 src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/old_goals.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/old_goals.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
diff -r f2924219125e -r fedb8be05f24 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/sign.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/sign.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson and Markus Wenzel
 
 Logical signature content: naming conventions, concrete syntax, type
diff -r f2924219125e -r fedb8be05f24 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/simplifier.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/simplifier.ML
-    ID:         $Id$
     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
 
 Generic simplifier, suitable for most logics (see also
diff -r f2924219125e -r fedb8be05f24 src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/subgoal.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/subgoal.ML
-    ID:         $Id$
     Author:     Makarius
 
 Tactical operations depending on local subgoal structure.
diff -r f2924219125e -r fedb8be05f24 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/theory.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/theory.ML
-    ID:         $Id$
     Author:     Lawrence C Paulson and Markus Wenzel
 
 Logical theory content: axioms, definitions, and begin/end wrappers.
diff -r f2924219125e -r fedb8be05f24 src/Pure/type_infer.ML
--- a/src/Pure/type_infer.ML	Wed Jan 21 22:26:49 2009 +0100
+++ b/src/Pure/type_infer.ML	Wed Jan 21 23:21:44 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/type_infer.ML
-    ID:         $Id$
     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
 
 Simple type inference.