eliminated theory CPure;
authorwenzelm
Sun May 18 17:03:20 2008 +0200 (2008-05-18)
changeset 26957e3f04fdd994d
parent 26956 1309a6a0a29f
child 26958 ed3a58a9eae1
eliminated theory CPure;
doc-src/IsarImplementation/Thy/base.thy
doc-src/IsarRef/Thy/intro.thy
doc-src/IsarRef/Thy/pure.thy
doc-src/IsarRef/Thy/syntax.thy
src/HOL/Complex/ex/linreif.ML
src/HOL/Complex/ex/mireif.ML
src/HOL/HOL.thy
src/HOL/Modelcheck/MuckeSyn.thy
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/refute.ML
src/HOL/ex/Higher_Order_Logic.thy
src/Pure/CPure.thy
src/Pure/IsaMakefile
src/Pure/Thy/present.ML
src/Pure/context.ML
src/Pure/pure_setup.ML
src/Tools/Compute_Oracle/Compute_Oracle.thy
     1.1 --- a/doc-src/IsarImplementation/Thy/base.thy	Sun May 18 17:03:16 2008 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/base.thy	Sun May 18 17:03:20 2008 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4  (* $Id$ *)
     1.5  
     1.6  theory base
     1.7 -imports CPure
     1.8 +imports Pure
     1.9  uses "../../antiquote_setup.ML"
    1.10  begin
    1.11  
     2.1 --- a/doc-src/IsarRef/Thy/intro.thy	Sun May 18 17:03:16 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/intro.thy	Sun May 18 17:03:20 2008 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  (* $Id$ *)
     2.5  
     2.6  theory intro
     2.7 -imports CPure
     2.8 +imports Pure
     2.9  begin
    2.10  
    2.11  chapter {* Introduction *}
     3.1 --- a/doc-src/IsarRef/Thy/pure.thy	Sun May 18 17:03:16 2008 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/pure.thy	Sun May 18 17:03:20 2008 +0200
     3.3 @@ -1,7 +1,7 @@
     3.4  (* $Id$ *)
     3.5  
     3.6  theory pure
     3.7 -imports CPure
     3.8 +imports Pure
     3.9  begin
    3.10  
    3.11  chapter {* Basic language elements \label{ch:pure-syntax} *}
     4.1 --- a/doc-src/IsarRef/Thy/syntax.thy	Sun May 18 17:03:16 2008 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/syntax.thy	Sun May 18 17:03:20 2008 +0200
     4.3 @@ -1,7 +1,7 @@
     4.4  (* $Id$ *)
     4.5  
     4.6  theory "syntax"
     4.7 -imports CPure
     4.8 +imports Pure
     4.9  begin
    4.10  
    4.11  chapter {* Syntax primitives *}
     5.1 --- a/src/HOL/Complex/ex/linreif.ML	Sun May 18 17:03:16 2008 +0200
     5.2 +++ b/src/HOL/Complex/ex/linreif.ML	Sun May 18 17:03:20 2008 +0200
     5.3 @@ -35,7 +35,7 @@
     5.4          | _ => error "num_of_term: unsupported Multiplication")
     5.5        | Const("RealDef.real",_) $ Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
     5.6        | Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
     5.7 -      | _ => error ("num_of_term: unknown term " ^ Syntax.string_of_term_global CPure.thy t);
     5.8 +      | _ => error ("num_of_term: unknown term " ^ Syntax.string_of_term_global Pure.thy t);
     5.9  
    5.10  (* pseudo reification : term -> fm *)
    5.11  fun fm_of_term vs t = 
    5.12 @@ -56,7 +56,7 @@
    5.13  	E(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
    5.14        | Const("All",_)$Term.Abs(xn,xT,p) => 
    5.15  	A(fm_of_term (map (fn(v,n) => (v,1+ n)) vs) p)
    5.16 -      | _ => error ("fm_of_term : unknown term!" ^ Syntax.string_of_term_global CPure.thy t);
    5.17 +      | _ => error ("fm_of_term : unknown term!" ^ Syntax.string_of_term_global Pure.thy t);
    5.18  
    5.19  
    5.20  fun start_vs t =
     6.1 --- a/src/HOL/Complex/ex/mireif.ML	Sun May 18 17:03:16 2008 +0200
     6.2 +++ b/src/HOL/Complex/ex/mireif.ML	Sun May 18 17:03:20 2008 +0200
     6.3 @@ -34,7 +34,7 @@
     6.4        | Const("RealDef.real",_)$ (Const (@{const_name "RComplete.ceiling"},_)$ t') => Neg(Floor (Neg (num_of_term vs t')))
     6.5        | Const("RealDef.real",_) $ Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
     6.6        | Const (@{const_name "Int.number_of"},_)$t' => C (HOLogic.dest_numeral t')
     6.7 -      | _ => error ("num_of_term: unknown term " ^ Syntax.string_of_term_global CPure.thy t);
     6.8 +      | _ => error ("num_of_term: unknown term " ^ Syntax.string_of_term_global Pure.thy t);
     6.9          
    6.10  
    6.11  (* pseudo reification : term -> fm *)
    6.12 @@ -58,7 +58,7 @@
    6.13          E (fm_of_term (map (fn (v, n) => (v, Suc n)) vs) p)
    6.14        | Const("All",_)$Abs(xn,xT,p) => 
    6.15          A (fm_of_term (map (fn(v, n) => (v, Suc n)) vs) p)
    6.16 -      | _ => error ("fm_of_term : unknown term!" ^ Syntax.string_of_term_global CPure.thy t);
    6.17 +      | _ => error ("fm_of_term : unknown term!" ^ Syntax.string_of_term_global Pure.thy t);
    6.18  
    6.19  fun start_vs t =
    6.20      let val fs = term_frees t
     7.1 --- a/src/HOL/HOL.thy	Sun May 18 17:03:16 2008 +0200
     7.2 +++ b/src/HOL/HOL.thy	Sun May 18 17:03:20 2008 +0200
     7.3 @@ -6,7 +6,7 @@
     7.4  header {* The basis of Higher-Order Logic *}
     7.5  
     7.6  theory HOL
     7.7 -imports CPure
     7.8 +imports Pure
     7.9  uses
    7.10    ("hologic.ML")
    7.11    "~~/src/Tools/IsaPlanner/zipper.ML"
     8.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy	Sun May 18 17:03:16 2008 +0200
     8.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy	Sun May 18 17:03:20 2008 +0200
     8.3 @@ -164,7 +164,7 @@
     8.4  
     8.5  (* transforming fun-defs into lambda-defs *)
     8.6  
     8.7 -val [eq] = goal CPure.thy "(!! x. f x == g x) ==> f == g";
     8.8 +val [eq] = goal Pure.thy "(!! x. f x == g x) ==> f == g";
     8.9   by (rtac (extensional eq) 1);
    8.10  qed "ext_rl";
    8.11  
     9.1 --- a/src/HOL/Tools/metis_tools.ML	Sun May 18 17:03:16 2008 +0200
     9.2 +++ b/src/HOL/Tools/metis_tools.ML	Sun May 18 17:03:20 2008 +0200
     9.3 @@ -166,9 +166,9 @@
     9.4      let val trands = terms_of rands
     9.5      in  if length trands = nargs then Term (list_comb(rator, trands))
     9.6          else error
     9.7 -          ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global CPure.thy rator ^
     9.8 +          ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
     9.9              " expected " ^ Int.toString nargs ^
    9.10 -            " received " ^ commas (map (Syntax.string_of_term_global CPure.thy) trands))
    9.11 +            " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
    9.12      end;
    9.13  
    9.14  (*Instantiate constant c with the supplied types, but if they don't match its declared
    10.1 --- a/src/HOL/Tools/record_package.ML	Sun May 18 17:03:16 2008 +0200
    10.2 +++ b/src/HOL/Tools/record_package.ML	Sun May 18 17:03:20 2008 +0200
    10.3 @@ -110,7 +110,7 @@
    10.4      (tracing str; map (trace_thm "") thms);
    10.5  
    10.6  fun trace_term str t =
    10.7 -    tracing (str ^ Syntax.string_of_term_global CPure.thy t);
    10.8 +    tracing (str ^ Syntax.string_of_term_global Pure.thy t);
    10.9  
   10.10  (* timing *)
   10.11  
    11.1 --- a/src/HOL/Tools/refute.ML	Sun May 18 17:03:16 2008 +0200
    11.2 +++ b/src/HOL/Tools/refute.ML	Sun May 18 17:03:20 2008 +0200
    11.3 @@ -456,7 +456,7 @@
    11.4            (* schematic type variable not instantiated *)
    11.5            raise REFUTE ("monomorphic_term",
    11.6              "no substitution for type variable " ^ fst (fst v) ^
    11.7 -            " in term " ^ Syntax.string_of_term_global CPure.thy t)
    11.8 +            " in term " ^ Syntax.string_of_term_global Pure.thy t)
    11.9          | SOME typ =>
   11.10            typ)) t;
   11.11  
    12.1 --- a/src/HOL/ex/Higher_Order_Logic.thy	Sun May 18 17:03:16 2008 +0200
    12.2 +++ b/src/HOL/ex/Higher_Order_Logic.thy	Sun May 18 17:03:20 2008 +0200
    12.3 @@ -5,7 +5,7 @@
    12.4  
    12.5  header {* Foundations of HOL *}
    12.6  
    12.7 -theory Higher_Order_Logic imports CPure begin
    12.8 +theory Higher_Order_Logic imports Pure begin
    12.9  
   12.10  text {*
   12.11    The following theory development demonstrates Higher-Order Logic
    13.1 --- a/src/Pure/CPure.thy	Sun May 18 17:03:16 2008 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,21 +0,0 @@
    13.4 -(*  Title:      Pure/CPure.thy
    13.5 -    ID:         $Id$
    13.6 -
    13.7 -The CPure theory -- Pure with alternative application syntax.
    13.8 -*)
    13.9 -
   13.10 -theory CPure
   13.11 -imports Pure
   13.12 -begin
   13.13 -
   13.14 -no_syntax
   13.15 -  "_appl" :: "('b => 'a) => args => logic"  ("(1_/(1'(_')))" [1000, 0] 1000)
   13.16 -  "_appl" :: "('b => 'a) => args => aprop"  ("(1_/(1'(_')))" [1000, 0] 1000)
   13.17 -
   13.18 -syntax
   13.19 -  "" :: "'a => cargs"  ("_")
   13.20 -  "_cargs" :: "'a => cargs => cargs"  ("_/ _" [1000, 1000] 1000)
   13.21 -  "_applC" :: "('b => 'a) => cargs => logic"  ("(1_/ _)" [1000, 1000] 999)
   13.22 -  "_applC" :: "('b => 'a) => cargs => aprop"  ("(1_/ _)" [1000, 1000] 999)
   13.23 -
   13.24 -end
    14.1 --- a/src/Pure/IsaMakefile	Sun May 18 17:03:16 2008 +0200
    14.2 +++ b/src/Pure/IsaMakefile	Sun May 18 17:03:20 2008 +0200
    14.3 @@ -23,7 +23,7 @@
    14.4  
    14.5  Pure: $(OUT)/Pure$(ML_SUFFIX)
    14.6  
    14.7 -$(OUT)/Pure$(ML_SUFFIX): CPure.thy General/ROOT.ML General/alist.ML	\
    14.8 +$(OUT)/Pure$(ML_SUFFIX): General/ROOT.ML General/alist.ML		\
    14.9    General/balanced_tree.ML General/basics.ML General/buffer.ML		\
   14.10    General/file.ML General/graph.ML General/heap.ML General/history.ML	\
   14.11    General/integer.ML General/markup.ML General/name_space.ML		\
    15.1 --- a/src/Pure/Thy/present.ML	Sun May 18 17:03:16 2008 +0200
    15.2 +++ b/src/Pure/Thy/present.ML	Sun May 18 17:03:20 2008 +0200
    15.3 @@ -76,17 +76,13 @@
    15.4  structure BrowserInfoData = TheoryDataFun
    15.5  (
    15.6    type T = {name: string, session: string list, is_local: bool};
    15.7 -  val empty = {name = "", session = [], is_local = false}: T;
    15.8 +  val empty = {name = Context.PureN, session = [], is_local = false}: T;
    15.9    val copy = I;
   15.10    fun extend _ = empty;
   15.11    fun merge _ _ = empty;
   15.12  );
   15.13  
   15.14 -fun get_info thy =
   15.15 -  if member (op =) [Context.PureN, Context.CPureN] (Context.theory_name thy)
   15.16 -  then {name = Context.PureN, session = [], is_local = false}
   15.17 -  else BrowserInfoData.get thy;
   15.18 -
   15.19 +val get_info = BrowserInfoData.get;
   15.20  val session_name = #name o get_info;
   15.21  
   15.22  
    16.1 --- a/src/Pure/context.ML	Sun May 18 17:03:16 2008 +0200
    16.2 +++ b/src/Pure/context.ML	Sun May 18 17:03:20 2008 +0200
    16.3 @@ -23,7 +23,6 @@
    16.4    val ancestors_of: theory -> theory list
    16.5    val is_stale: theory -> bool
    16.6    val PureN: string
    16.7 -  val CPureN: string
    16.8    val is_draft: theory -> bool
    16.9    val exists_name: string -> theory -> bool
   16.10    val names_of: theory -> string list
   16.11 @@ -197,7 +196,6 @@
   16.12  (* names *)
   16.13  
   16.14  val PureN = "Pure";
   16.15 -val CPureN = "CPure";
   16.16  
   16.17  val draftN = "#";
   16.18  fun draft_id (_, name) = (name = draftN);
   16.19 @@ -340,18 +338,15 @@
   16.20  (* named theory nodes *)
   16.21  
   16.22  fun merge_thys pp (thy1, thy2) =
   16.23 -  if exists_name CPureN thy1 <> exists_name CPureN thy2 then
   16.24 -    error "Cannot merge Pure and CPure developments"
   16.25 -  else
   16.26 -    let
   16.27 -      val (ids, iids) = check_merge thy1 thy2;
   16.28 -      val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
   16.29 -      val ancestry = make_ancestry [] [];
   16.30 -      val history = make_history "" 0 [];
   16.31 -      val thy' = NAMED_CRITICAL "theory" (fn () =>
   16.32 -       (check_thy thy1; check_thy thy2;
   16.33 -        create_thy draftN NONE (serial (), draftN) ids iids data ancestry history))
   16.34 -    in thy' end;
   16.35 +  let
   16.36 +    val (ids, iids) = check_merge thy1 thy2;
   16.37 +    val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
   16.38 +    val ancestry = make_ancestry [] [];
   16.39 +    val history = make_history "" 0 [];
   16.40 +    val thy' = NAMED_CRITICAL "theory" (fn () =>
   16.41 +     (check_thy thy1; check_thy thy2;
   16.42 +      create_thy draftN NONE (serial (), draftN) ids iids data ancestry history))
   16.43 +  in thy' end;
   16.44  
   16.45  fun maximal_thys thys =
   16.46    thys |> filter (fn thy => not (exists (fn thy' => proper_subthy (thy, thy')) thys));
    17.1 --- a/src/Pure/pure_setup.ML	Sun May 18 17:03:16 2008 +0200
    17.2 +++ b/src/Pure/pure_setup.ML	Sun May 18 17:03:20 2008 +0200
    17.3 @@ -25,9 +25,6 @@
    17.4  Context.set_thread_data NONE;
    17.5  ThyInfo.register_theory Pure.thy;
    17.6  
    17.7 -use_thy "CPure";
    17.8 -structure CPure = struct val thy = theory "CPure" end;
    17.9 -
   17.10  
   17.11  (* ML toplevel pretty printing *)
   17.12  
    18.1 --- a/src/Tools/Compute_Oracle/Compute_Oracle.thy	Sun May 18 17:03:16 2008 +0200
    18.2 +++ b/src/Tools/Compute_Oracle/Compute_Oracle.thy	Sun May 18 17:03:20 2008 +0200
    18.3 @@ -5,10 +5,10 @@
    18.4  Steven Obua's evaluator.
    18.5  *)
    18.6  
    18.7 -theory Compute_Oracle imports CPure
    18.8 +theory Compute_Oracle imports Pure
    18.9  uses "am.ML" "am_compiler.ML" "am_interpreter.ML" "am_ghc.ML" "am_sml.ML" "report.ML" "compute.ML" "linker.ML"
   18.10  begin
   18.11  
   18.12 -setup {* Compute.setup_compute; *}
   18.13 +setup {* Compute.setup_compute *}
   18.14  
   18.15  end
   18.16 \ No newline at end of file