src/HOL/Spec_Check/gen_construction.ML

--- a/src/HOL/Spec_Check/gen_construction.ML	Thu May 30 20:57:55 2013 +0200
+++ b/src/HOL/Spec_Check/gen_construction.ML	Thu May 30 21:28:54 2013 +0200
@@ -9,8 +9,8 @@
 sig
   val register : string * (string * string) -> theory -> theory
   type mltype
-  val parse_pred : string -> string * mltype;
-  val build_check : theory -> string -> mltype * string -> string
+  val parse_pred : string -> string * mltype
+  val build_check : Proof.context -> string -> mltype * string -> string
   (*val safe_check : string -> mltype * string -> string*)
   val string_of_bool : bool -> string
   val string_of_ref : ('a -> string) -> 'a Unsynchronized.ref -> string
@@ -111,8 +111,8 @@
   fun merge data : T = Symtab.merge (K true) data
 )
 
-fun data_of thy tycon =
-  (case Symtab.lookup (Data.get thy) tycon of
+fun data_of ctxt tycon =
+  (case Symtab.lookup (Data.get (Proof_Context.theory_of ctxt)) tycon of
     SOME data => data
   | NONE => error ("No generator and printer defined for ML type constructor " ^ quote tycon))
 
@@ -129,44 +129,50 @@
   | combine dict dicts = enclose "(" ")" dict ^ " " ^ enclose "(" ")" (commas dicts)
 
 fun compose_generator _ Var = "Generator.int"
-  | compose_generator thy (Con (s, types)) =
-      combine (generator_of thy s) (map (compose_generator thy) types)
-  | compose_generator thy (Tuple t) =
-    let
-      fun tuple_body t = space_implode ""
-        (map (fn (ty, n) => "val (x" ^ string_of_int n ^ ", r" ^ string_of_int n ^ ") = " ^
-        compose_generator thy ty ^ " r" ^ string_of_int (n - 1) ^ " ") (t ~~ (1 upto (length t))))
-      fun tuple_ret a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
-    in "fn r0 => let " ^ tuple_body t ^
-      "in ((" ^ tuple_ret (length t) ^ "), r" ^ string_of_int (length t) ^ ") end" end;
+  | compose_generator ctxt (Con (s, types)) =
+      combine (generator_of ctxt s) (map (compose_generator ctxt) types)
+  | compose_generator ctxt (Tuple t) =
+      let
+        fun tuple_body t = space_implode ""
+          (map (fn (ty, n) => "val (x" ^ string_of_int n ^ ", r" ^ string_of_int n ^ ") = " ^
+          compose_generator ctxt ty ^ " r" ^ string_of_int (n - 1) ^ " ") (t ~~ (1 upto (length t))))
+        fun tuple_ret a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
+      in
+        "fn r0 => let " ^ tuple_body t ^
+        "in ((" ^ tuple_ret (length t) ^ "), r" ^ string_of_int (length t) ^ ") end"
+      end;
 
 fun compose_printer _ Var = "Int.toString"
-  | compose_printer thy (Con (s, types)) =
-      combine (printer_of thy s) (map (compose_printer thy) types)
-  | compose_printer thy (Tuple t) =
-    let
-      fun tuple_head a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
-      fun tuple_body t = space_implode " ^ \", \" ^ "
-        (map (fn (ty, n) => "(" ^ compose_printer thy ty ^ ") x" ^ string_of_int n)
-        (t ~~ (1 upto (length t))))
-    in "fn (" ^ tuple_head (length t) ^ ") => \"(\" ^ " ^ tuple_body t ^ " ^ \")\"" end;
+  | compose_printer ctxt (Con (s, types)) =
+      combine (printer_of ctxt s) (map (compose_printer ctxt) types)
+  | compose_printer ctxt (Tuple t) =
+      let
+        fun tuple_head a = commas (map (fn n => "x" ^ string_of_int n) (1 upto a))
+        fun tuple_body t = space_implode " ^ \", \" ^ "
+          (map (fn (ty, n) => "(" ^ compose_printer ctxt ty ^ ") x" ^ string_of_int n)
+          (t ~~ (1 upto (length t))))
+      in "fn (" ^ tuple_head (length t) ^ ") => \"(\" ^ " ^ tuple_body t ^ " ^ \")\"" end;
 
 (*produce compilable string*)
-fun build_check thy name (ty, spec) = "Spec_Check.checkGen (ML_Context.the_generic_context ()) ("
-  ^ compose_generator thy ty ^ ", SOME (" ^ compose_printer thy ty ^ ")) (\""
+fun build_check ctxt name (ty, spec) =
+  "Spec_Check.checkGen (ML_Context.the_local_context ()) ("
+  ^ compose_generator ctxt ty ^ ", SOME (" ^ compose_printer ctxt ty ^ ")) (\""
   ^ name ^ "\", Property.pred (" ^ spec ^ "));";
 
 (*produce compilable string - non-eqtype functions*)
 (*
 fun safe_check name (ty, spec) =
   let
-    val default = case AList.lookup (op =) (!gen_table) "->"
-      of NONE => ("gen_function_rand", "fn (_, _) => fn _ => \"fn\"")
-      | SOME entry => entry
-  in (gen_table := AList.update (op =) ("->", ("gen_function_safe", "fn (_, _) => fn _ => \"fn\""))
-   (!gen_table);
+    val default =
+      (case AList.lookup (op =) (!gen_table) "->" of
+        NONE => ("gen_function_rand", "fn (_, _) => fn _ => \"fn\"")
+      | SOME entry => entry)
+  in
+   (gen_table :=
+     AList.update (op =) ("->", ("gen_function_safe", "fn (_, _) => fn _ => \"fn\"")) (!gen_table);
     build_check name (ty, spec) before
-    gen_table := AList.update (op =) ("->", default) (!gen_table)) end;
+    gen_table := AList.update (op =) ("->", default) (!gen_table))
+  end;
 *)
 
 end;