added generic_setup, add_oracle (from isar_thy.ML);
authorwenzelm
Tue Sep 13 22:19:26 2005 +0200 (2005-09-13)
changeset 1734292504e2f6c07
parent 17341 ca0e5105c4b1
child 17343 098db1bc1e59
added generic_setup, add_oracle (from isar_thy.ML);
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/pure_thy.ML	Tue Sep 13 22:19:25 2005 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Tue Sep 13 22:19:26 2005 +0200
     1.3 @@ -72,6 +72,8 @@
     1.4      theory -> theory * thm list list
     1.5    val add_defss_i: bool -> ((bstring * term list) * theory attribute list) list ->
     1.6      theory -> theory * thm list list
     1.7 +  val generic_setup: string -> theory -> theory
     1.8 +  val add_oracle: bstring * string * string -> theory -> theory
     1.9  end;
    1.10  
    1.11  structure PureThy: PURE_THY =
    1.12 @@ -445,6 +447,33 @@
    1.13  
    1.14  
    1.15  
    1.16 +(*** ML setup ***)
    1.17 +
    1.18 +(* generic_setup *)
    1.19 +
    1.20 +val generic_setup =
    1.21 +  Context.use_let "val setup: (theory -> theory) list" "Library.apply setup";
    1.22 +
    1.23 +
    1.24 +(* add_oracle *)
    1.25 +
    1.26 +fun add_oracle (name, T, oracle) =
    1.27 +  let val txt =
    1.28 +    "local\n\
    1.29 +    \  type T = " ^ T ^ ";\n\
    1.30 +    \  val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
    1.31 +    \  val name = " ^ quote name ^ ";\n\
    1.32 +    \  exception Arg of T;\n\
    1.33 +    \  val _ = Context.>> (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x));\n\
    1.34 +    \  val thy = Context.the_context ();\n\
    1.35 +    \  val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\
    1.36 +    \in\n\
    1.37 +    \  fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\
    1.38 +    \end;\n";
    1.39 +  in Context.use_mltext_theory txt false end;
    1.40 +
    1.41 +
    1.42 +
    1.43  (*** the ProtoPure theory ***)
    1.44  
    1.45  val aT = TFree ("'a", []);