# HG changeset patch
# User wenzelm
# Date 1251809106 -7200
# Node ID a393b7e2a2f8c3ae8722d9fd945e5674906535ec
# Parent  87f0e1b2d3f2bf08a8b208524827b89c07f9881a
modernized Thy_Header;

diff -r 87f0e1b2d3f2 -r a393b7e2a2f8 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Sep 01 13:31:22 2009 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 01 14:45:06 2009 +0200
@@ -30,7 +30,7 @@
 
 val _ =
   OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin)
-    (ThyHeader.args >> (Toplevel.print oo IsarCmd.init_theory));
+    (Thy_Header.args >> (Toplevel.print oo IsarCmd.init_theory));
 
 val _ =
   OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
diff -r 87f0e1b2d3f2 -r a393b7e2a2f8 src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Tue Sep 01 13:31:22 2009 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Tue Sep 01 14:45:06 2009 +0200
@@ -20,7 +20,7 @@
 fun badcmd text = [D.Badcmd {text = text}];
 
 fun thy_begin text =
-  (case try (ThyHeader.read Position.none) (Source.of_string text) of
+  (case try (Thy_Header.read Position.none) (Source.of_string text) of
     NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
   | SOME (name, imports, _) =>
        D.Opentheory {thyname = SOME name, parentnames = imports, text = text})
diff -r 87f0e1b2d3f2 -r a393b7e2a2f8 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Tue Sep 01 13:31:22 2009 +0200
+++ b/src/Pure/Thy/thy_header.ML	Tue Sep 01 14:45:06 2009 +0200
@@ -11,7 +11,7 @@
   val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list
 end;
 
-structure ThyHeader: THY_HEADER =
+structure Thy_Header: THY_HEADER =
 struct
 
 structure T = OuterLex;
diff -r 87f0e1b2d3f2 -r a393b7e2a2f8 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Tue Sep 01 13:31:22 2009 +0200
+++ b/src/Pure/Thy/thy_header.scala	Tue Sep 01 14:45:06 2009 +0200
@@ -7,7 +7,7 @@
 package isabelle
 
 
-object ThyHeader
+object Thy_Header
 {
   val HEADER = "header"
   val THEORY = "theory"
diff -r 87f0e1b2d3f2 -r a393b7e2a2f8 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Tue Sep 01 13:31:22 2009 +0200
+++ b/src/Pure/Thy/thy_load.ML	Tue Sep 01 14:45:06 2009 +0200
@@ -109,7 +109,7 @@
     val master as (path, _) = check_thy dir name;
     val text = explode (File.read path);
     val (name', imports, uses) =
-      ThyHeader.read (Path.position path) (Source.of_list_limited 8000 text);
+      Thy_Header.read (Path.position path) (Source.of_list_limited 8000 text);
     val _ = check_name name name';
     val uses = map (Path.explode o #1) uses;
   in {master = master, text = text, imports = imports, uses = uses} end;