# HG changeset patch
# User wenzelm
# Date 1211123000 -7200
# Node ID e3f04fdd994d358929cd24db212bf26c58a02998
# Parent  1309a6a0a29f1b3a89189f37c0c510b4076e6526
eliminated theory CPure;

diff -r 1309a6a0a29f -r e3f04fdd994d doc-src/IsarImplementation/Thy/base.thy
--- a/doc-src/IsarImplementation/Thy/base.thy	Sun May 18 17:03:16 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/base.thy	Sun May 18 17:03:20 2008 +0200
@@ -2,7 +2,7 @@
 (* $Id$ *)
 
 theory base
-imports CPure
+imports Pure
 uses "../../antiquote_setup.ML"
 begin
 
diff -r 1309a6a0a29f -r e3f04fdd994d doc-src/IsarRef/Thy/intro.thy
--- a/doc-src/IsarRef/Thy/intro.thy	Sun May 18 17:03:16 2008 +0200
+++ b/doc-src/IsarRef/Thy/intro.thy	Sun May 18 17:03:20 2008 +0200
@@ -1,7 +1,7 @@
 (* $Id$ *)
 
 theory intro
-imports CPure
+imports Pure
 begin
 
 chapter {* Introduction *}
diff -r 1309a6a0a29f -r e3f04fdd994d doc-src/IsarRef/Thy/pure.thy
--- a/doc-src/IsarRef/Thy/pure.thy	Sun May 18 17:03:16 2008 +0200
+++ b/doc-src/IsarRef/Thy/pure.thy	Sun May 18 17:03:20 2008 +0200
@@ -1,7 +1,7 @@
 (* $Id$ *)
 
 theory pure
-imports CPure
+imports Pure
 begin
 
 chapter {* Basic language elements \label{ch:pure-syntax} *}
diff -r 1309a6a0a29f -r e3f04fdd994d doc-src/IsarRef/Thy/syntax.thy
--- a/doc-src/IsarRef/Thy/syntax.thy	Sun May 18 17:03:16 2008 +0200
+++ b/doc-src/IsarRef/Thy/syntax.thy	Sun May 18 17:03:20 2008 +0200
@@ -1,7 +1,7 @@
 (* $Id$ *)
 
 theory "syntax"
-imports CPure
+imports Pure
 begin
 
 chapter {* Syntax primitives *}
diff -r 1309a6a0a29f -r e3f04fdd994d src/HOL/Complex/ex/linreif.ML
--- a/src/HOL/Complex/ex/linreif.ML	Sun May 18 17:03:16 2008 +0200
+++ b/src/HOL/Complex/ex/linreif.ML	Sun May 18 17:03:20 2008 +0200
@@ -35,7 +35,7 @@
         | _ => error "num_of_term: unsupported Multiplication")
       | Const("RealDef.real",_) $ Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
       | Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
-      | _ => error ("num_of_term: unknown term " ^ Syntax.string_of_term_global CPure.thy t);
+      | _ => error ("num_of_term: unknown term " ^ Syntax.string_of_term_global Pure.thy t);
 
 (* pseudo reification : term -> fm *)
 fun fm_of_term vs t = 
@@ -56,7 +56,7 @@
 	E(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
       | Const("All",_)$Term.Abs(xn,xT,p) => 
 	A(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
-      | _ => error ("fm_of_term : unknown term!" ^ Syntax.string_of_term_global CPure.thy t);
+      | _ => error ("fm_of_term : unknown term!" ^ Syntax.string_of_term_global Pure.thy t);
 
 
 fun start_vs t =
diff -r 1309a6a0a29f -r e3f04fdd994d src/HOL/Complex/ex/mireif.ML
--- a/src/HOL/Complex/ex/mireif.ML	Sun May 18 17:03:16 2008 +0200
+++ b/src/HOL/Complex/ex/mireif.ML	Sun May 18 17:03:20 2008 +0200
@@ -34,7 +34,7 @@
       | Const("RealDef.real",_)$ (Const (@{const_name "RComplete.ceiling"},_)$ t') => Neg(Floor (Neg (num_of_term vs t')))
       | Const("RealDef.real",_) $ Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
       | Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
-      | _ => error ("num_of_term: unknown term " ^ Syntax.string_of_term_global CPure.thy t);
+      | _ => error ("num_of_term: unknown term " ^ Syntax.string_of_term_global Pure.thy t);
         
 
 (* pseudo reification : term -> fm *)
@@ -58,7 +58,7 @@
         E (fm_of_term (map (fn (v, n) => (v, Suc n)) vs) p)
       | Const("All",_)$Abs(xn,xT,p) => 
         A (fm_of_term (map (fn(v, n) => (v, Suc n)) vs) p)
-      | _ => error ("fm_of_term : unknown term!" ^ Syntax.string_of_term_global CPure.thy t);
+      | _ => error ("fm_of_term : unknown term!" ^ Syntax.string_of_term_global Pure.thy t);
 
 fun start_vs t =
     let val fs = term_frees t
diff -r 1309a6a0a29f -r e3f04fdd994d src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun May 18 17:03:16 2008 +0200
+++ b/src/HOL/HOL.thy	Sun May 18 17:03:20 2008 +0200
@@ -6,7 +6,7 @@
 header {* The basis of Higher-Order Logic *}
 
 theory HOL
-imports CPure
+imports Pure
 uses
   ("hologic.ML")
   "~~/src/Tools/IsaPlanner/zipper.ML"
diff -r 1309a6a0a29f -r e3f04fdd994d src/HOL/Modelcheck/MuckeSyn.thy
--- a/src/HOL/Modelcheck/MuckeSyn.thy	Sun May 18 17:03:16 2008 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy	Sun May 18 17:03:20 2008 +0200
@@ -164,7 +164,7 @@
 
 (* transforming fun-defs into lambda-defs *)
 
-val [eq] = goal CPure.thy "(!! x. f x == g x) ==> f == g";
+val [eq] = goal Pure.thy "(!! x. f x == g x) ==> f == g";
  by (rtac (extensional eq) 1);
 qed "ext_rl";
 
diff -r 1309a6a0a29f -r e3f04fdd994d src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Sun May 18 17:03:16 2008 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Sun May 18 17:03:20 2008 +0200
@@ -166,9 +166,9 @@
     let val trands = terms_of rands
     in  if length trands = nargs then Term (list_comb(rator, trands))
         else error
-          ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global CPure.thy rator ^
+          ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
             " expected " ^ Int.toString nargs ^
-            " received " ^ commas (map (Syntax.string_of_term_global CPure.thy) trands))
+            " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
     end;
 
 (*Instantiate constant c with the supplied types, but if they don't match its declared
diff -r 1309a6a0a29f -r e3f04fdd994d src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Sun May 18 17:03:16 2008 +0200
+++ b/src/HOL/Tools/record_package.ML	Sun May 18 17:03:20 2008 +0200
@@ -110,7 +110,7 @@
     (tracing str; map (trace_thm "") thms);
 
 fun trace_term str t =
-    tracing (str ^ Syntax.string_of_term_global CPure.thy t);
+    tracing (str ^ Syntax.string_of_term_global Pure.thy t);
 
 (* timing *)
 
diff -r 1309a6a0a29f -r e3f04fdd994d src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Sun May 18 17:03:16 2008 +0200
+++ b/src/HOL/Tools/refute.ML	Sun May 18 17:03:20 2008 +0200
@@ -456,7 +456,7 @@
           (* schematic type variable not instantiated *)
           raise REFUTE ("monomorphic_term",
             "no substitution for type variable " ^ fst (fst v) ^
-            " in term " ^ Syntax.string_of_term_global CPure.thy t)
+            " in term " ^ Syntax.string_of_term_global Pure.thy t)
         | SOME typ =>
           typ)) t;
 
diff -r 1309a6a0a29f -r e3f04fdd994d src/HOL/ex/Higher_Order_Logic.thy
--- a/src/HOL/ex/Higher_Order_Logic.thy	Sun May 18 17:03:16 2008 +0200
+++ b/src/HOL/ex/Higher_Order_Logic.thy	Sun May 18 17:03:20 2008 +0200
@@ -5,7 +5,7 @@
 
 header {* Foundations of HOL *}
 
-theory Higher_Order_Logic imports CPure begin
+theory Higher_Order_Logic imports Pure begin
 
 text {*
   The following theory development demonstrates Higher-Order Logic
diff -r 1309a6a0a29f -r e3f04fdd994d src/Pure/CPure.thy
--- a/src/Pure/CPure.thy	Sun May 18 17:03:16 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-(*  Title:      Pure/CPure.thy
-    ID:         $Id$
-
-The CPure theory -- Pure with alternative application syntax.
-*)
-
-theory CPure
-imports Pure
-begin
-
-no_syntax
-  "_appl" :: "('b => 'a) => args => logic"  ("(1_/(1'(_')))" [1000, 0] 1000)
-  "_appl" :: "('b => 'a) => args => aprop"  ("(1_/(1'(_')))" [1000, 0] 1000)
-
-syntax
-  "" :: "'a => cargs"  ("_")
-  "_cargs" :: "'a => cargs => cargs"  ("_/ _" [1000, 1000] 1000)
-  "_applC" :: "('b => 'a) => cargs => logic"  ("(1_/ _)" [1000, 1000] 999)
-  "_applC" :: "('b => 'a) => cargs => aprop"  ("(1_/ _)" [1000, 1000] 999)
-
-end
diff -r 1309a6a0a29f -r e3f04fdd994d src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sun May 18 17:03:16 2008 +0200
+++ b/src/Pure/IsaMakefile	Sun May 18 17:03:20 2008 +0200
@@ -23,7 +23,7 @@
 
 Pure: $(OUT)/Pure$(ML_SUFFIX)
 
-$(OUT)/Pure$(ML_SUFFIX): CPure.thy General/ROOT.ML General/alist.ML	\
+$(OUT)/Pure$(ML_SUFFIX): General/ROOT.ML General/alist.ML		\
   General/balanced_tree.ML General/basics.ML General/buffer.ML		\
   General/file.ML General/graph.ML General/heap.ML General/history.ML	\
   General/integer.ML General/markup.ML General/name_space.ML		\
diff -r 1309a6a0a29f -r e3f04fdd994d src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sun May 18 17:03:16 2008 +0200
+++ b/src/Pure/Thy/present.ML	Sun May 18 17:03:20 2008 +0200
@@ -76,17 +76,13 @@
 structure BrowserInfoData = TheoryDataFun
 (
   type T = {name: string, session: string list, is_local: bool};
-  val empty = {name = "", session = [], is_local = false}: T;
+  val empty = {name = Context.PureN, session = [], is_local = false}: T;
   val copy = I;
   fun extend _ = empty;
   fun merge _ _ = empty;
 );
 
-fun get_info thy =
-  if member (op =) [Context.PureN, Context.CPureN] (Context.theory_name thy)
-  then {name = Context.PureN, session = [], is_local = false}
-  else BrowserInfoData.get thy;
-
+val get_info = BrowserInfoData.get;
 val session_name = #name o get_info;
 
 
diff -r 1309a6a0a29f -r e3f04fdd994d src/Pure/context.ML
--- a/src/Pure/context.ML	Sun May 18 17:03:16 2008 +0200
+++ b/src/Pure/context.ML	Sun May 18 17:03:20 2008 +0200
@@ -23,7 +23,6 @@
   val ancestors_of: theory -> theory list
   val is_stale: theory -> bool
   val PureN: string
-  val CPureN: string
   val is_draft: theory -> bool
   val exists_name: string -> theory -> bool
   val names_of: theory -> string list
@@ -197,7 +196,6 @@
 (* names *)
 
 val PureN = "Pure";
-val CPureN = "CPure";
 
 val draftN = "#";
 fun draft_id (_, name) = (name = draftN);
@@ -340,18 +338,15 @@
 (* named theory nodes *)
 
 fun merge_thys pp (thy1, thy2) =
-  if exists_name CPureN thy1 <> exists_name CPureN thy2 then
-    error "Cannot merge Pure and CPure developments"
-  else
-    let
-      val (ids, iids) = check_merge thy1 thy2;
-      val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
-      val ancestry = make_ancestry [] [];
-      val history = make_history "" 0 [];
-      val thy' = NAMED_CRITICAL "theory" (fn () =>
-       (check_thy thy1; check_thy thy2;
-        create_thy draftN NONE (serial (), draftN) ids iids data ancestry history))
-    in thy' end;
+  let
+    val (ids, iids) = check_merge thy1 thy2;
+    val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
+    val ancestry = make_ancestry [] [];
+    val history = make_history "" 0 [];
+    val thy' = NAMED_CRITICAL "theory" (fn () =>
+     (check_thy thy1; check_thy thy2;
+      create_thy draftN NONE (serial (), draftN) ids iids data ancestry history))
+  in thy' end;
 
 fun maximal_thys thys =
   thys |> filter (fn thy => not (exists (fn thy' => proper_subthy (thy, thy')) thys));
diff -r 1309a6a0a29f -r e3f04fdd994d src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Sun May 18 17:03:16 2008 +0200
+++ b/src/Pure/pure_setup.ML	Sun May 18 17:03:20 2008 +0200
@@ -25,9 +25,6 @@
 Context.set_thread_data NONE;
 ThyInfo.register_theory Pure.thy;
 
-use_thy "CPure";
-structure CPure = struct val thy = theory "CPure" end;
-
 
 (* ML toplevel pretty printing *)
 
diff -r 1309a6a0a29f -r e3f04fdd994d src/Tools/Compute_Oracle/Compute_Oracle.thy
--- a/src/Tools/Compute_Oracle/Compute_Oracle.thy	Sun May 18 17:03:16 2008 +0200
+++ b/src/Tools/Compute_Oracle/Compute_Oracle.thy	Sun May 18 17:03:20 2008 +0200
@@ -5,10 +5,10 @@
 Steven Obua's evaluator.
 *)
 
-theory Compute_Oracle imports CPure
+theory Compute_Oracle imports Pure
 uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML"
 begin
 
-setup {* Compute.setup_compute; *}
+setup {* Compute.setup_compute *}
 
 end
\ No newline at end of file