# 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