# HG changeset patch
# User wenzelm
# Date 899148815 -7200
# Node ID e443bc494604c17aadc27273811f5ac48a4b829a
# Parent  4dc26d3e87227275142ebefc24f9f763a64de794
moved actual (C)Pure theories to pure.ML;

diff -r 4dc26d3e8722 -r e443bc494604 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Mon Jun 29 21:33:25 1998 +0200
+++ b/src/Pure/IsaMakefile	Mon Jun 29 21:33:35 1998 +0200
@@ -36,7 +36,7 @@
   Thy/thy_info.ML Thy/thy_parse.ML Thy/thy_read.ML Thy/thy_scan.ML \
   Thy/thy_syn.ML Thy/use.ML attribute.ML axclass.ML basis.ML deriv.ML \
   display.ML drule.ML envir.ML goals.ML install_pp.ML library.ML \
-  logic.ML net.ML pattern.ML pure_thy.ML search.ML sign.ML sorts.ML \
+  logic.ML net.ML pattern.ML pure.ML pure_thy.ML search.ML sign.ML sorts.ML \
   tactic.ML tctical.ML term.ML theory.ML theory_data.ML thm.ML type.ML \
   type_infer.ML unify.ML
 	@./mk
diff -r 4dc26d3e8722 -r e443bc494604 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Jun 29 21:33:25 1998 +0200
+++ b/src/Pure/ROOT.ML	Mon Jun 29 21:33:35 1998 +0200
@@ -46,6 +46,7 @@
 use "tactic.ML";
 use "goals.ML";
 use "axclass.ML";
+use "pure.ML";
 
 (*theory parser and loader*)
 cd "Thy";
diff -r 4dc26d3e8722 -r e443bc494604 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Mon Jun 29 21:33:25 1998 +0200
+++ b/src/Pure/goals.ML	Mon Jun 29 21:33:35 1998 +0200
@@ -98,7 +98,7 @@
     ref((fn _=> error"No goal has been supplied in subgoal module") 
        : bool*thm->thm);
 
-val dummy = trivial(read_cterm (sign_of Pure.thy)
+val dummy = trivial(read_cterm (sign_of ProtoPure.thy)
     ("PROP No_goal_has_been_supplied",propT));
 
 (*List of previous goal stacks, for the undo operation.  Set by setstate. 
diff -r 4dc26d3e8722 -r e443bc494604 src/Pure/pure.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/pure.ML	Mon Jun 29 21:33:35 1998 +0200
@@ -0,0 +1,27 @@
+(*  Title:      Pure/pure.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+The actual Pure and CPure theories.
+*)
+
+structure Pure =
+struct
+
+val thy =
+  PureThy.begin_theory "Pure" [ProtoPure.thy]
+  |> Theory.add_syntax Syntax.pure_appl_syntax
+  |> PureThy.end_theory;
+
+end;
+
+
+structure CPure =
+struct
+
+val thy =
+  PureThy.begin_theory "CPure" [ProtoPure.thy]
+  |> Theory.add_syntax Syntax.pure_applC_syntax
+  |> PureThy.end_theory;
+
+end;