--- 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
--- 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 *}
--- 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} *}
--- 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 *}
--- 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 =
--- 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
--- 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"
--- 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";
--- 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
--- 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 *)
--- 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;
--- 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
--- 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
--- 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 \
--- 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;
--- 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));
--- 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 *)
--- 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