--- a/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Mon Sep 01 17:34:03 2014 +0200
+++ b/src/HOL/SPARK/Examples/Gcd/Greatest_Common_Divisor.thy Mon Sep 01 18:42:02 2014 +0200
@@ -4,7 +4,7 @@
*)
theory Greatest_Common_Divisor
-imports SPARK GCD
+imports "../../SPARK" GCD
begin
spark_proof_functions
--- a/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Mon Sep 01 17:34:03 2014 +0200
+++ b/src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy Mon Sep 01 18:42:02 2014 +0200
@@ -4,7 +4,7 @@
*)
theory Longest_Increasing_Subsequence
-imports SPARK
+imports "../../SPARK"
begin
text {*
--- a/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy Mon Sep 01 17:34:03 2014 +0200
+++ b/src/HOL/SPARK/Examples/Sqrt/Sqrt.thy Mon Sep 01 18:42:02 2014 +0200
@@ -4,7 +4,7 @@
*)
theory Sqrt
-imports SPARK
+imports "../../SPARK"
begin
spark_open "sqrt/isqrt"
--- a/src/HOL/SPARK/Manual/Complex_Types.thy Mon Sep 01 17:34:03 2014 +0200
+++ b/src/HOL/SPARK/Manual/Complex_Types.thy Mon Sep 01 18:42:02 2014 +0200
@@ -1,8 +1,8 @@
theory Complex_Types
-imports SPARK
+imports "../SPARK"
begin
-datatype day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
+datatype_new day = Mon | Tue | Wed | Thu | Fri | Sat | Sun
record two_fields =
Field1 :: "int \<times> day \<Rightarrow> int"
--- a/src/HOL/SPARK/Manual/Proc1.thy Mon Sep 01 17:34:03 2014 +0200
+++ b/src/HOL/SPARK/Manual/Proc1.thy Mon Sep 01 18:42:02 2014 +0200
@@ -1,5 +1,5 @@
theory Proc1
-imports SPARK
+imports "../SPARK"
begin
spark_open "loop_invariant/proc1"
--- a/src/HOL/SPARK/Manual/Proc2.thy Mon Sep 01 17:34:03 2014 +0200
+++ b/src/HOL/SPARK/Manual/Proc2.thy Mon Sep 01 18:42:02 2014 +0200
@@ -1,5 +1,5 @@
theory Proc2
-imports SPARK
+imports "../SPARK"
begin
spark_open "loop_invariant/proc2"
--- a/src/HOL/SPARK/Manual/Reference.thy Mon Sep 01 17:34:03 2014 +0200
+++ b/src/HOL/SPARK/Manual/Reference.thy Mon Sep 01 18:42:02 2014 +0200
@@ -1,6 +1,6 @@
(*<*)
theory Reference
-imports SPARK
+imports "../SPARK"
begin
syntax (my_constrain output)
--- a/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy Mon Sep 01 17:34:03 2014 +0200
+++ b/src/HOL/SPARK/Manual/Simple_Greatest_Common_Divisor.thy Mon Sep 01 18:42:02 2014 +0200
@@ -4,7 +4,7 @@
*)
theory Simple_Greatest_Common_Divisor
-imports SPARK GCD
+imports "../SPARK" GCD
begin
spark_proof_functions
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Mon Sep 01 17:34:03 2014 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Mon Sep 01 18:42:02 2014 +0200
@@ -173,8 +173,8 @@
fun add_enum_type tyname tyname' thy =
let
- val {case_name, ...} = the (Old_Datatype_Data.get_info thy tyname');
- val cs = map Const (the (Old_Datatype_Data.get_constrs thy tyname'));
+ val {case_name, ...} = the (BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting tyname');
+ val cs = map Const (the (BNF_LFP_Compat.get_constrs thy tyname'));
val k = length cs;
val T = Type (tyname', []);
val p = Const (@{const_name pos}, T --> HOLogic.intT);
@@ -209,8 +209,8 @@
(fn _ =>
rtac @{thm subset_antisym} 1 THEN
rtac @{thm subsetI} 1 THEN
- Old_Datatype_Aux.exh_tac (K (#exhaust (Old_Datatype_Data.the_info
- (Proof_Context.theory_of lthy) tyname'))) 1 THEN
+ Old_Datatype_Aux.exh_tac (K (#exhaust (BNF_LFP_Compat.the_info
+ (Proof_Context.theory_of lthy) BNF_LFP_Compat.Keep_Nesting tyname'))) 1 THEN
ALLGOALS (asm_full_simp_tac lthy));
val finite_UNIV = Goal.prove lthy [] []
@@ -320,14 +320,14 @@
val tyname = Sign.full_name thy tyb
in
(thy |>
- Old_Datatype.add_datatype {strict = true, quiet = true}
+ BNF_LFP_Compat.add_datatype BNF_LFP_Compat.Keep_Nesting
[((tyb, [], NoSyn),
map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
add_enum_type s tyname,
tyname)
end
| SOME (T as Type (tyname, []), cmap) =>
- (case Old_Datatype_Data.get_constrs thy tyname of
+ (case BNF_LFP_Compat.get_constrs thy tyname of
NONE => assoc_ty_err thy T s "is not a datatype"
| SOME cs =>
let val (prfx', _) = strip_prfx s
@@ -338,7 +338,7 @@
| SOME msg => assoc_ty_err thy T s msg
end)
| SOME (T, _) => assoc_ty_err thy T s "is not a datatype");
- val cs = map Const (the (Old_Datatype_Data.get_constrs thy' tyname));
+ val cs = map Const (the (BNF_LFP_Compat.get_constrs thy' tyname));
in
((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
fold Name.declare els ctxt),
@@ -888,7 +888,7 @@
handle Symtab.DUP _ => error ("SPARK type " ^ s ^
" already associated with type")) |>
(fn thy' =>
- case Old_Datatype_Data.get_constrs thy' tyname of
+ case BNF_LFP_Compat.get_constrs thy' tyname of
NONE => (case get_record_info thy' T of
NONE => thy'
| SOME {fields, ...} =>
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 01 17:34:03 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Sep 01 18:42:02 2014 +0200
@@ -203,7 +203,7 @@
end;
fun get_info_of_new_datatype thy nesting_pref T_name =
- let val lthy = Named_Target.theory_init thy in
+ let val lthy = Proof_Context.init_global thy in
AList.lookup (op =) (infos_of_new_datatype_mutual_cluster lthy nesting_pref T_name) T_name
end;