--- a/Admin/isatest/isatest-makedist Wed Mar 21 16:53:24 2012 +0100
+++ b/Admin/isatest/isatest-makedist Wed Mar 21 23:41:22 2012 +0100
@@ -108,8 +108,8 @@
$SSH macbroy24 "$MAKEALL $HOME/settings/at64-poly"
sleep 15
$SSH macbroy2 "
- $MAKEALL $HOME/settings/mac-poly64-M4 -l . full;
- $MAKEALL $HOME/settings/mac-poly64-M8 -l . full;
+ $MAKEALL -l . full $HOME/settings/mac-poly64-M4;
+ $MAKEALL -l . full $HOME/settings/mac-poly64-M8;
$MAKEALL $HOME/settings/mac-poly-M4;
$MAKEALL $HOME/settings/mac-poly-M8"
sleep 15
--- a/etc/isar-keywords-ZF.el Wed Mar 21 16:53:24 2012 +0100
+++ b/etc/isar-keywords-ZF.el Wed Mar 21 23:41:22 2012 +0100
@@ -226,6 +226,7 @@
"if"
"imports"
"in"
+ "includes"
"induction"
"infix"
"infixl"
--- a/etc/isar-keywords.el Wed Mar 21 16:53:24 2012 +0100
+++ b/etc/isar-keywords.el Wed Mar 21 23:41:22 2012 +0100
@@ -305,6 +305,7 @@
"if"
"imports"
"in"
+ "includes"
"infix"
"infixl"
"infixr"
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Mar 21 23:41:22 2012 +0100
@@ -341,7 +341,7 @@
let
fun default_prover_name () =
hd (#provers (Sledgehammer_Isar.default_params ctxt []))
- handle Empty => error "No ATP available."
+ handle List.Empty => error "No ATP available."
fun get_prover name =
(name, Sledgehammer_Run.get_minimizing_prover ctxt
Sledgehammer_Provers.Normal name)
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Wed Mar 21 23:41:22 2012 +0100
@@ -83,7 +83,7 @@
(cut_inst_tac_term' [(x,s)] exists_fresh' 1 THEN
rtac fs_name_thm 1 THEN
etac exE 1) thm
- handle Empty => all_tac thm (* if we collected no variables then we do nothing *)
+ handle List.Empty => all_tac thm (* if we collected no variables then we do nothing *)
end;
fun get_inner_fresh_fun (Bound j) = NONE
--- a/src/HOL/SPARK/Tools/spark_commands.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Wed Mar 21 23:41:22 2012 +0100
@@ -61,7 +61,7 @@
Specification.theorem Thm.theoremK NONE
(fn thmss => (Local_Theory.background_theory
(SPARK_VCs.mark_proved vc_name (flat thmss))))
- (Binding.name vc_name, []) ctxt stmt true lthy
+ (Binding.name vc_name, []) [] ctxt stmt true lthy
end;
fun string_of_status NONE = "(unproved)"
--- a/src/HOL/Tools/Function/pat_completeness.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/HOL/Tools/Function/pat_completeness.ML Wed Mar 21 23:41:22 2012 +0100
@@ -143,7 +143,7 @@
val (qss, x_pats) = split_list (map pat_of cases)
val xs = map fst (hd x_pats)
- handle Empty => raise COMPLETENESS
+ handle List.Empty => raise COMPLETENESS
val patss = map (map snd) x_pats
val complete_thm = prove_completeness thy xs thesis qss patss
--- a/src/HOL/Tools/inductive_realizer.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Mar 21 23:41:22 2012 +0100
@@ -505,7 +505,7 @@
(case HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of thm)) of
[_] => [pred_of (HOLogic.dest_Trueprop (hd (prems_of thm)))]
| xs => map (pred_of o fst o HOLogic.dest_imp) xs)
- handle TERM _ => err () | Empty => err ();
+ handle TERM _ => err () | List.Empty => err ();
in
add_ind_realizers (hd sets)
(case arg of
--- a/src/HOL/Tools/recdef.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/HOL/Tools/recdef.ML Wed Mar 21 23:41:22 2012 +0100
@@ -266,7 +266,7 @@
" in recdef definition of " ^ quote name);
in
Specification.theorem "" NONE (K I)
- (Binding.conceal (Binding.name bname), atts) []
+ (Binding.conceal (Binding.name bname), atts) [] []
(Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
end;
--- a/src/Provers/Arith/fast_lin_arith.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Wed Mar 21 23:41:22 2012 +0100
@@ -384,7 +384,7 @@
fun extract_first p =
let
fun extract xs (y::ys) = if p y then (y, xs @ ys) else extract (y::xs) ys
- | extract xs [] = raise Empty
+ | extract xs [] = raise List.Empty
in extract [] end;
fun print_ineqs ctxt ineqs =
--- a/src/Pure/General/balanced_tree.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/General/balanced_tree.ML Wed Mar 21 23:41:22 2012 +0100
@@ -15,7 +15,7 @@
structure Balanced_Tree: BALANCED_TREE =
struct
-fun make _ [] = raise Empty
+fun make _ [] = raise List.Empty
| make _ [x] = x
| make f xs =
let
@@ -24,7 +24,7 @@
in f (make f ps, make f qs) end;
fun dest f n x =
- if n <= 0 then raise Empty
+ if n <= 0 then raise List.Empty
else if n = 1 then [x]
else
let
--- a/src/Pure/General/queue.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/General/queue.ML Wed Mar 21 23:41:22 2012 +0100
@@ -11,7 +11,7 @@
val is_empty: 'a T -> bool
val content: 'a T -> 'a list
val enqueue: 'a -> 'a T -> 'a T
- val dequeue: 'a T -> 'a * 'a T
+ val dequeue: 'a T -> 'a * 'a T (*exception List.Empty*)
end;
structure Queue: QUEUE =
@@ -30,6 +30,6 @@
fun dequeue (Queue (xs, y :: ys)) = (y, Queue (xs, ys))
| dequeue (Queue (xs as _ :: _, [])) = let val y :: ys = rev xs in (y, Queue ([], ys)) end
- | dequeue (Queue ([], [])) = raise Empty;
+ | dequeue (Queue ([], [])) = raise List.Empty;
end;
--- a/src/Pure/General/seq.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/General/seq.ML Wed Mar 21 23:41:22 2012 +0100
@@ -167,7 +167,7 @@
fun lift f xq y = map (fn x => f x y) xq;
fun lifts f xq y = maps (fn x => f x y) xq;
-fun singleton f x = f [x] |> map (fn [y] => y | _ => raise Empty);
+fun singleton f x = f [x] |> map (fn [y] => y | _ => raise List.Empty);
(*print a sequence, up to "count" elements*)
fun print print_elem count =
--- a/src/Pure/General/stack.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/General/stack.ML Wed Mar 21 23:41:22 2012 +0100
@@ -13,7 +13,7 @@
val map_top: ('a -> 'a) -> 'a T -> 'a T
val map_all: ('a -> 'a) -> 'a T -> 'a T
val push: 'a T -> 'a T
- val pop: 'a T -> 'a T (*exception Empty*)
+ val pop: 'a T -> 'a T (*exception List.Empty*)
end;
structure Stack: STACK =
@@ -34,6 +34,6 @@
fun push (x, xs) = (x, x :: xs);
fun pop (_, x :: xs) = (x, xs)
- | pop (_, []) = raise Empty;
+ | pop (_, []) = raise List.Empty;
end;
--- a/src/Pure/Isar/bundle.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/bundle.ML Wed Mar 21 23:41:22 2012 +0100
@@ -13,10 +13,14 @@
(binding * typ option * mixfix) list -> local_theory -> local_theory
val bundle_cmd: binding * (Facts.ref * Args.src list) list ->
(binding * string option * mixfix) list -> local_theory -> local_theory
- val include_: string -> Proof.state -> Proof.state
- val include_cmd: xstring * Position.T -> Proof.state -> Proof.state
- val including: string -> Proof.state -> Proof.state
- val including_cmd: xstring * Position.T -> Proof.state -> Proof.state
+ val includes: string list -> Proof.context -> Proof.context
+ val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
+ val context_includes: string list -> generic_theory -> local_theory
+ val context_includes_cmd: (xstring * Position.T) list -> generic_theory -> local_theory
+ val include_: string list -> Proof.state -> Proof.state
+ val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
+ val including: string list -> Proof.state -> Proof.state
+ val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
val print_bundles: Proof.context -> unit
end;
@@ -78,20 +82,42 @@
end;
-(* include bundle *)
+(* include bundles *)
+
+local
+
+fun gen_includes prep args ctxt =
+ let
+ val decls = maps (the_bundle ctxt o prep ctxt) args;
+ val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt);
+ val note = ((Binding.empty, []), map (apsnd (map attrib)) decls);
+ in #2 (Proof_Context.note_thmss "" [note] ctxt) end;
-fun gen_include prep raw_name =
- Proof.map_context (fn ctxt =>
- let
- val bundle = the_bundle ctxt (prep ctxt raw_name);
- val attrib = Attrib.attribute_i (Proof_Context.theory_of ctxt);
- val note = ((Binding.empty, []), map (apsnd (map attrib)) bundle);
- in #2 (Proof_Context.note_thmss "" [note] ctxt) end);
+fun gen_context prep args (Context.Theory thy) =
+ Named_Target.theory_init thy
+ |> Local_Theory.target (gen_includes prep args)
+ |> Local_Theory.restore
+ | gen_context prep args (Context.Proof lthy) =
+ Named_Target.assert lthy
+ |> gen_includes prep args
+ |> Local_Theory.open_target (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy);
+
+in
-fun include_ name = Proof.assert_forward #> gen_include (K I) name #> Proof.put_facts NONE;
-fun include_cmd name = Proof.assert_forward #> gen_include check name #> Proof.put_facts NONE;
-fun including name = Proof.assert_backward #> gen_include (K I) name;
-fun including_cmd name = Proof.assert_backward #> gen_include check name;
+val includes = gen_includes (K I);
+val includes_cmd = gen_includes check;
+
+val context_includes = gen_context (K I);
+val context_includes_cmd = gen_context check;
+
+fun include_ bs = Proof.assert_forward #> Proof.map_context (includes bs) #> Proof.reset_facts;
+fun include_cmd bs =
+ Proof.assert_forward #> Proof.map_context (includes_cmd bs) #> Proof.reset_facts;
+
+fun including bs = Proof.assert_backward #> Proof.map_context (includes bs);
+fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs);
+
+end;
(* print_bundles *)
--- a/src/Pure/Isar/class.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/class.ML Wed Mar 21 23:41:22 2012 +0100
@@ -512,6 +512,8 @@
fun instantiation (tycos, vs, sort) thy =
let
+ val naming = Sign.naming_of thy;
+
val _ = if null tycos then error "At least one arity must be given" else ();
val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort);
fun get_param tyco (param, (_, (c, ty))) =
@@ -545,7 +547,7 @@
|> Overloading.activate_improvable_syntax
|> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check)
|> synchronize_inst_syntax
- |> Local_Theory.init NONE ""
+ |> Local_Theory.init naming
{define = Generic_Target.define foundation,
notes = Generic_Target.notes
(fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
--- a/src/Pure/Isar/expression.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/expression.ML Wed Mar 21 23:41:22 2012 +0100
@@ -860,7 +860,7 @@
fun after_qed witss eqns =
(Proof.map_context o Context.proof_map)
(note_eqns_register deps witss attrss eqns export export')
- #> Proof.put_facts NONE;
+ #> Proof.reset_facts;
in
state
|> Element.witness_local_proof_eqs after_qed "interpret" propss eqns goal_ctxt int
--- a/src/Pure/Isar/isar_syn.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML Wed Mar 21 23:41:22 2012 +0100
@@ -16,7 +16,7 @@
"\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
"advanced", "and", "assumes", "attach", "begin", "binder",
"constrains", "defines", "fixes", "for", "identifier", "if",
- "imports", "in", "infix", "infixl", "infixr", "is", "keywords",
+ "imports", "in", "includes", "infix", "infixl", "infixr", "is", "keywords",
"notes", "obtains", "open", "output", "overloaded", "pervasive",
"shows", "structure", "unchecked", "uses", "where", "|"]));
@@ -25,16 +25,17 @@
(** init and exit **)
val _ =
- Outer_Syntax.command ("theory", Keyword.tag_theory Keyword.thy_begin) "begin theory"
+ Outer_Syntax.command ("theory", Keyword.tag_theory Keyword.thy_begin) "begin theory context"
(Thy_Header.args >> (fn header =>
Toplevel.print o
Toplevel.init_theory
(fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
val _ =
- Outer_Syntax.command ("end", Keyword.tag_theory Keyword.thy_end) "end (local) theory"
+ Outer_Syntax.command ("end", Keyword.tag_theory Keyword.thy_end) "end context"
(Scan.succeed
- (Toplevel.exit o Toplevel.end_local_theory o Toplevel.end_proof (K Proof.end_notepad)));
+ (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
+ Toplevel.end_proof (K Proof.end_notepad)));
@@ -406,14 +407,6 @@
(fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
-(* local theories *)
-
-val _ =
- Outer_Syntax.command ("context", Keyword.thy_decl) "enter local theory context"
- (Parse.position Parse.xname --| Parse.begin >> (fn name =>
- Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));
-
-
(* bundled declarations *)
val _ =
@@ -424,12 +417,14 @@
val _ =
Outer_Syntax.command ("include", Keyword.prf_decl)
"include declarations from bundle in proof body"
- (Parse.position Parse.xname >> (Toplevel.print oo (Toplevel.proof o Bundle.include_cmd)));
+ (Scan.repeat1 (Parse.position Parse.xname)
+ >> (Toplevel.print oo (Toplevel.proof o Bundle.include_cmd)));
val _ =
Outer_Syntax.command ("including", Keyword.prf_decl)
"include declarations from bundle in goal refinement"
- (Parse.position Parse.xname >> (Toplevel.print oo (Toplevel.proof o Bundle.including_cmd)));
+ (Scan.repeat1 (Parse.position Parse.xname)
+ >> (Toplevel.print oo (Toplevel.proof o Bundle.including_cmd)));
val _ =
Outer_Syntax.improper_command ("print_bundles", Keyword.diag) "print bundles of declarations"
@@ -437,6 +432,16 @@
Toplevel.keep (Bundle.print_bundles o Toplevel.context_of)));
+(* local theories *)
+
+val _ =
+ Outer_Syntax.command ("context", Keyword.thy_decl) "begin local theory context"
+ ((Parse_Spec.includes >> (Toplevel.open_target o Bundle.context_includes_cmd) ||
+ Parse.position Parse.xname >> (fn name =>
+ Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)))
+ --| Parse.begin);
+
+
(* locales *)
val locale_val =
@@ -544,10 +549,12 @@
else (kind, Keyword.thy_goal))
("state " ^ (if schematic then "schematic " ^ kind else kind))
(Scan.optional (Parse_Spec.opt_thm_name ":" --|
- Scan.ahead (Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
- Parse_Spec.general_statement >> (fn (a, (elems, concl)) =>
+ Scan.ahead (Parse_Spec.includes >> K "" ||
+ Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
+ Scan.optional Parse_Spec.includes [] --
+ Parse_Spec.general_statement >> (fn ((a, includes), (elems, concl)) =>
((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
- kind NONE (K I) a elems concl)));
+ kind NONE (K I) a includes elems concl)));
val _ = gen_theorem false Thm.theoremK;
val _ = gen_theorem false Thm.lemmaK;
@@ -557,8 +564,7 @@
val _ = gen_theorem true Thm.corollaryK;
val _ =
- Outer_Syntax.local_theory_to_proof ("notepad", Keyword.thy_decl)
- "Isar proof state as formal notepad, without any result"
+ Outer_Syntax.local_theory_to_proof ("notepad", Keyword.thy_decl) "begin proof context"
(Parse.begin >> K Proof.begin_notepad);
val _ =
--- a/src/Pure/Isar/local_defs.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/local_defs.ML Wed Mar 21 23:41:22 2012 +0100
@@ -173,7 +173,7 @@
val is_trivial = Pattern.aeconv o Logic.dest_equals o Thm.prop_of;
-fun trans_list _ _ [] = raise Empty
+fun trans_list _ _ [] = raise List.Empty
| trans_list trans ctxt (th :: raw_eqs) =
(case filter_out is_trivial raw_eqs of
[] => th
--- a/src/Pure/Isar/local_theory.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/local_theory.ML Wed Mar 21 23:41:22 2012 +0100
@@ -10,7 +10,12 @@
signature LOCAL_THEORY =
sig
type operations
- val affirm: local_theory -> local_theory
+ val map_contexts: (Proof.context -> Proof.context) -> local_theory -> local_theory
+ val assert: local_theory -> local_theory
+ val level: Proof.context -> int
+ val assert_bottom: bool -> local_theory -> local_theory
+ val open_target: Name_Space.naming -> operations -> local_theory -> local_theory
+ val close_target: local_theory -> local_theory
val naming_of: local_theory -> Name_Space.naming
val full_name: local_theory -> binding -> string
val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
@@ -25,11 +30,11 @@
val background_theory: (theory -> theory) -> local_theory -> local_theory
val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
- val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
val propagate_ml_env: generic_theory -> generic_theory
val standard_morphism: local_theory -> Proof.context -> morphism
val target_morphism: local_theory -> morphism
val global_morphism: local_theory -> morphism
+ val operations_of: local_theory -> operations
val define: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory
val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
@@ -49,7 +54,7 @@
val class_alias: binding -> class -> local_theory -> local_theory
val type_alias: binding -> string -> local_theory -> local_theory
val const_alias: binding -> string -> local_theory -> local_theory
- val init: serial option -> string -> operations -> Proof.context -> local_theory
+ val init: Name_Space.naming -> operations -> Proof.context -> local_theory
val restore: local_theory -> local_theory
val exit: local_theory -> Proof.context
val exit_global: local_theory -> theory
@@ -76,35 +81,56 @@
pretty: local_theory -> Pretty.T list,
exit: local_theory -> Proof.context};
-datatype lthy = LThy of
+type lthy =
{naming: Name_Space.naming,
- theory_prefix: string,
operations: operations,
target: Proof.context};
-fun make_lthy (naming, theory_prefix, operations, target) =
- LThy {naming = naming, theory_prefix = theory_prefix,
- operations = operations, target = target};
+fun make_lthy (naming, operations, target) : lthy =
+ {naming = naming, operations = operations, target = target};
(* context data *)
structure Data = Proof_Data
(
- type T = lthy option;
- fun init _ = NONE;
+ type T = lthy list;
+ fun init _ = [];
);
-fun get_lthy lthy =
- (case Data.get lthy of
- NONE => error "No local theory context"
- | SOME (LThy data) => data);
+fun map_contexts f =
+ (Data.map o map) (fn {naming, operations, target} => make_lthy (naming, operations, f target))
+ #> f;
+
+fun assert lthy =
+ if null (Data.get lthy) then error "Missing local theory context" else lthy;
+
+val get_lthy = hd o Data.get o assert;
+
+fun map_lthy f = assert #>
+ Data.map (fn {naming, operations, target} :: parents =>
+ make_lthy (f (naming, operations, target)) :: parents);
+
+
+(* nested structure *)
-fun map_lthy f lthy =
- let val {naming, theory_prefix, operations, target} = get_lthy lthy
- in Data.put (SOME (make_lthy (f (naming, theory_prefix, operations, target)))) lthy end;
+val level = length o Data.get;
-val affirm = tap get_lthy;
+fun assert_bottom b lthy =
+ let
+ val _ = assert lthy;
+ val b' = level lthy <= 1;
+ in
+ if b andalso not b' then error "Not at bottom of local theory nesting"
+ else if not b andalso b' then error "Already at bottom of local theory nesting"
+ else lthy
+ end;
+
+fun open_target naming operations target = assert target
+ |> Data.map (cons (make_lthy (naming, operations, target)));
+
+fun close_target lthy =
+ assert_bottom false lthy |> Data.map tl;
(* naming *)
@@ -112,8 +138,7 @@
val naming_of = #naming o get_lthy;
val full_name = Name_Space.full_name o naming_of;
-fun map_naming f = map_lthy (fn (naming, theory_prefix, operations, target) =>
- (f naming, theory_prefix, operations, target));
+fun map_naming f = map_lthy (fn (naming, operations, target) => (f naming, operations, target));
val conceal = map_naming Name_Space.conceal;
val new_group = map_naming Name_Space.new_group;
@@ -126,8 +151,7 @@
val target_of = #target o get_lthy;
-fun map_target f = map_lthy (fn (naming, theory_prefix, operations, target) =>
- (naming, theory_prefix, operations, f target));
+fun map_target f = map_lthy (fn (naming, operations, target) => (naming, operations, f target));
(* substructure mappings *)
@@ -135,9 +159,7 @@
fun raw_theory_result f lthy =
let
val (res, thy') = f (Proof_Context.theory_of lthy);
- val lthy' = lthy
- |> map_target (Proof_Context.transfer thy')
- |> Proof_Context.transfer thy';
+ val lthy' = map_contexts (Proof_Context.transfer thy') lthy;
in (res, lthy') end;
fun raw_theory f = #2 o raw_theory_result (f #> pair ());
@@ -163,18 +185,18 @@
val thy' = Proof_Context.theory_of ctxt';
val lthy' = lthy
|> map_target (K ctxt')
- |> Proof_Context.transfer thy';
+ |> map_contexts (Proof_Context.transfer thy');
in (res, lthy') end;
fun target f = #2 o target_result (f #> pair ());
-fun map_contexts f =
- background_theory (Context.theory_map f) #>
- target (Context.proof_map f) #>
- Context.proof_map f;
-
fun propagate_ml_env (context as Context.Proof lthy) =
- Context.Proof (map_contexts (ML_Env.inherit context) lthy)
+ let val inherit = ML_Env.inherit context in
+ lthy
+ |> background_theory (Context.theory_map inherit)
+ |> map_contexts (Context.proof_map inherit)
+ |> Context.Proof
+ end
| propagate_ml_env context = context;
@@ -185,15 +207,21 @@
Morphism.binding_morphism (Name_Space.transform_binding (naming_of lthy));
fun target_morphism lthy = standard_morphism lthy (target_of lthy);
+
fun global_morphism lthy =
standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
-(* primitive operations *)
+
+(** operations **)
+
+val operations_of = #operations o get_lthy;
-fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
-fun operation1 f x = operation (fn ops => f ops x);
-fun operation2 f x y lthy = operation (fn ops => f ops x y) lthy;
+
+(* primitives *)
+
+fun operation f lthy = f (operations_of lthy) lthy;
+fun operation2 f x y = operation (fn ops => f ops x y);
val pretty = operation #pretty;
val abbrev = apsnd checkpoint ooo operation2 #abbrev;
@@ -203,8 +231,7 @@
val declaration = checkpoint ooo operation2 #declaration;
-
-(** basic derived operations **)
+(* basic derived operations *)
val notes = notes_kind "";
fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
@@ -246,21 +273,15 @@
(* init *)
-fun init group theory_prefix operations target =
- let val naming =
- Sign.naming_of (Proof_Context.theory_of target)
- |> Name_Space.set_group group
- |> Name_Space.mandatory_path theory_prefix;
- in
- target |> Data.map
- (fn NONE => SOME (make_lthy (naming, theory_prefix, operations, target))
- | SOME _ => error "Local theory already initialized")
- |> checkpoint
- end;
+fun init naming operations target =
+ target |> Data.map
+ (fn [] => [make_lthy (naming, operations, target)]
+ | _ => error "Local theory already initialized")
+ |> checkpoint;
fun restore lthy =
- let val {naming, theory_prefix, operations, target} = get_lthy lthy
- in init (Name_Space.get_group naming) theory_prefix operations target end;
+ let val {naming, operations, target} = get_lthy lthy
+ in init naming operations target end;
(* exit *)
--- a/src/Pure/Isar/named_target.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/named_target.ML Wed Mar 21 23:41:22 2012 +0100
@@ -2,16 +2,17 @@
Author: Makarius
Author: Florian Haftmann, TU Muenchen
-Targets for theory, locale and class.
+Targets for theory, locale, class -- at the bottom the nested structure.
*)
signature NAMED_TARGET =
sig
+ val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
+ val assert: local_theory -> local_theory
val init: (local_theory -> local_theory) -> string -> theory -> local_theory
val theory_init: theory -> local_theory
val reinit: local_theory -> local_theory -> local_theory
val context_cmd: xstring * Position.T -> theory -> local_theory
- val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
end;
structure Named_Target: NAMED_TARGET =
@@ -43,6 +44,10 @@
Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
{target = target, is_locale = is_locale, is_class = is_class});
+fun assert lthy =
+ if is_some (peek lthy) then lthy
+ else error "Not in a named target (global theory, locale, class)";
+
(* generic declarations *)
@@ -192,11 +197,13 @@
fun init before_exit target thy =
let
val ta = named_target thy target before_exit;
+ val naming = Sign.naming_of thy
+ |> Name_Space.mandatory_path (Long_Name.base_name target);
in
thy
|> init_context ta
|> Data.put (SOME ta)
- |> Local_Theory.init NONE (Long_Name.base_name target)
+ |> Local_Theory.init naming
{define = Generic_Target.define (target_foundation ta),
notes = Generic_Target.notes (target_notes ta),
abbrev = Generic_Target.abbrev (target_abbrev ta),
@@ -207,11 +214,9 @@
val theory_init = init I "";
-fun reinit lthy =
- (case Data.get lthy of
- SOME (Target {target, before_exit, ...}) =>
- init before_exit target o Local_Theory.exit_global
- | NONE => error "Not in a named target");
+val reinit =
+ Local_Theory.assert_bottom true #> Data.get #> the #>
+ (fn Target {target, before_exit, ...} => Local_Theory.exit_global #> init before_exit target);
fun context_cmd ("-", _) thy = init I "" thy
| context_cmd target thy = init I (Locale.check thy target) thy;
--- a/src/Pure/Isar/overloading.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/overloading.ML Wed Mar 21 23:41:22 2012 +0100
@@ -189,6 +189,7 @@
fun gen_overloading prep_const raw_overloading thy =
let
val ctxt = Proof_Context.init_global thy;
+ val naming = Sign.naming_of thy;
val _ = if null raw_overloading then error "At least one parameter must be given" else ();
val overloading = raw_overloading |> map (fn (v, const, checked) =>
(Term.dest_Const (prep_const ctxt const), (v, checked)));
@@ -200,7 +201,7 @@
|> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
|> activate_improvable_syntax
|> synchronize_syntax
- |> Local_Theory.init NONE ""
+ |> Local_Theory.init naming
{define = Generic_Target.define foundation,
notes = Generic_Target.notes
(fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
--- a/src/Pure/Isar/parse_spec.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/parse_spec.ML Wed Mar 21 23:41:22 2012 +0100
@@ -19,6 +19,7 @@
val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
val constdecl: (binding * string option * mixfix) parser
val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
+ val includes: (xstring * Position.T) list parser
val locale_mixfix: mixfix parser
val locale_fixes: (binding * string option * mixfix) list parser
val locale_insts: (string option list * (Attrib.binding * string) list) parser
@@ -79,6 +80,8 @@
(* locale and context elements *)
+val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.xname));
+
val locale_mixfix =
Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
Parse.mixfix;
--- a/src/Pure/Isar/proof.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/proof.ML Wed Mar 21 23:41:22 2012 +0100
@@ -23,7 +23,8 @@
val put_thms: bool -> string * thm list option -> state -> state
val the_facts: state -> thm list
val the_fact: state -> thm
- val put_facts: thm list option -> state -> state
+ val set_facts: thm list -> state -> state
+ val reset_facts: state -> state
val assert_forward: state -> state
val assert_chain: state -> state
val assert_forward_or_chain: state -> state
@@ -183,14 +184,14 @@
fun open_block (State st) = State (Stack.push st);
fun close_block (State st) = State (Stack.pop st)
- handle Empty => error "Unbalanced block parentheses";
+ handle List.Empty => error "Unbalanced block parentheses";
fun level (State st) = Stack.level st;
fun assert_bottom b state =
- let val b' = (level state <= 2) in
- if b andalso not b' then error "Not at bottom of proof!"
- else if not b andalso b' then error "Already at bottom of proof!"
+ let val b' = level state <= 2 in
+ if b andalso not b' then error "Not at bottom of proof"
+ else if not b andalso b' then error "Already at bottom of proof"
else state
end;
@@ -231,16 +232,19 @@
map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
put_thms true (Auto_Bind.thisN, facts);
+val set_facts = put_facts o SOME;
+val reset_facts = put_facts NONE;
+
fun these_factss more_facts (named_factss, state) =
- (named_factss, state |> put_facts (SOME (maps snd named_factss @ more_facts)));
+ (named_factss, state |> set_facts (maps snd named_factss @ more_facts));
fun export_facts inner outer =
(case get_facts inner of
- NONE => put_facts NONE outer
+ NONE => reset_facts outer
| SOME thms =>
thms
|> Proof_Context.export (context_of inner) (context_of outer)
- |> (fn ths => put_facts (SOME ths) outer));
+ |> (fn ths => set_facts ths outer));
(* mode *)
@@ -272,17 +276,20 @@
fun current_goal state =
(case current state of
{context, goal = SOME (Goal goal), ...} => (context, goal)
- | _ => error "No current goal!");
+ | _ => error "No current goal");
fun assert_current_goal g state =
let val g' = can current_goal state in
- if g andalso not g' then error "No goal in this block!"
- else if not g andalso g' then error "Goal present in this block!"
+ if g andalso not g' then error "No goal in this block"
+ else if not g andalso g' then error "Goal present in this block"
else state
end;
fun put_goal goal = map_current (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
+val set_goal = put_goal o SOME;
+val reset_goal = put_goal NONE;
+
val before_qed = #before_qed o #2 o current_goal;
@@ -298,7 +305,7 @@
in map_context f (State (nd, node' :: nodes')) end
| map_goal _ _ state = state;
-fun set_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) =>
+fun provide_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) =>
(statement, [], using, goal, before_qed, after_qed));
fun goal_message msg = map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) =>
@@ -412,10 +419,10 @@
|> ALLGOALS Goal.conjunction_tac
|> Seq.maps (fn goal =>
state
- |> Seq.lift set_goal (Goal.extract 1 n goal |> Seq.maps (Goal.conjunction_tac 1))
+ |> Seq.lift provide_goal (Goal.extract 1 n goal |> Seq.maps (Goal.conjunction_tac 1))
|> Seq.maps meth
|> Seq.maps (fn state' => state'
- |> Seq.lift set_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
+ |> Seq.lift provide_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
|> Seq.maps (apply_method true (K Method.succeed)));
fun apply_text cc text state =
@@ -471,7 +478,7 @@
in
raw_rules
|> Proof_Context.goal_export inner outer
- |> (fn rules => Seq.lift set_goal (EVERY (map refine rules) goal) state)
+ |> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state)
end;
end;
@@ -488,7 +495,7 @@
val ngoals = Thm.nprems_of goal;
val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
(Goal_Display.pretty_goals ctxt goal @
- [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])));
+ [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)")])));
val extra_hyps = Assumption.extra_hyps ctxt goal;
val _ = null extra_hyps orelse
@@ -548,7 +555,7 @@
state
|> assert_forward
|> map_context (bind true args #> snd)
- |> put_facts NONE;
+ |> reset_facts;
in
@@ -565,7 +572,7 @@
fun gen_write prep_arg mode args =
assert_forward
#> map_context (fn ctxt => ctxt |> Proof_Context.notation true mode (map (prep_arg ctxt) args))
- #> put_facts NONE;
+ #> reset_facts;
in
@@ -585,7 +592,7 @@
fun gen_fix prep_vars args =
assert_forward
#> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (prep_vars args ctxt)) ctxt))
- #> put_facts NONE;
+ #> reset_facts;
in
@@ -635,7 +642,7 @@
|-> (fn vars =>
map_context_result (prep_binds false (map swap raw_rhss))
#-> (fn rhss => map_context_result (Local_Defs.add_defs (vars ~~ (name_atts ~~ rhss)))))
- |-> (put_facts o SOME o map (#2 o #2))
+ |-> (set_facts o map (#2 o #2))
end;
in
@@ -652,7 +659,7 @@
(* chain *)
fun clean_facts ctxt =
- put_facts (SOME (filter_out Thm.is_dummy (the_facts ctxt))) ctxt;
+ set_facts (filter_out Thm.is_dummy (the_facts ctxt)) ctxt;
val chain =
assert_forward
@@ -660,7 +667,7 @@
#> enter_chain;
fun chain_facts facts =
- put_facts (SOME facts)
+ set_facts facts
#> chain;
@@ -765,15 +772,15 @@
val begin_block =
assert_forward
#> open_block
- #> put_goal NONE
+ #> reset_goal
#> open_block;
val next_block =
assert_forward
#> close_block
#> open_block
- #> put_goal NONE
- #> put_facts NONE;
+ #> reset_goal
+ #> reset_facts;
fun end_block state =
state
@@ -889,12 +896,12 @@
in
goal_state
|> map_context (init_context #> Variable.set_body true)
- |> put_goal (SOME (make_goal (statement, [], [], Goal.init goal, before_qed, after_qed')))
+ |> set_goal (make_goal (statement, [], [], Goal.init goal, before_qed, after_qed'))
|> map_context (Proof_Context.auto_bind_goal props)
|> chaining ? (`the_facts #-> using_facts)
- |> put_facts NONE
+ |> reset_facts
|> open_block
- |> put_goal NONE
+ |> reset_goal
|> enter_backward
|> not (null vars) ? refine_terms (length goal_propss)
|> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
--- a/src/Pure/Isar/specification.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/specification.ML Wed Mar 21 23:41:22 2012 +0100
@@ -60,19 +60,19 @@
bool -> local_theory -> (string * thm list) list * local_theory
val theorem: string -> Method.text option ->
(thm list list -> local_theory -> local_theory) -> Attrib.binding ->
- Element.context_i list -> Element.statement_i ->
+ string list -> Element.context_i list -> Element.statement_i ->
bool -> local_theory -> Proof.state
val theorem_cmd: string -> Method.text option ->
(thm list list -> local_theory -> local_theory) -> Attrib.binding ->
- Element.context list -> Element.statement ->
+ (xstring * Position.T) list -> Element.context list -> Element.statement ->
bool -> local_theory -> Proof.state
val schematic_theorem: string -> Method.text option ->
(thm list list -> local_theory -> local_theory) -> Attrib.binding ->
- Element.context_i list -> Element.statement_i ->
+ string list -> Element.context_i list -> Element.statement_i ->
bool -> local_theory -> Proof.state
val schematic_theorem_cmd: string -> Method.text option ->
(thm list list -> local_theory -> local_theory) -> Attrib.binding ->
- Element.context list -> Element.statement ->
+ (xstring * Position.T) list -> Element.context list -> Element.statement ->
bool -> local_theory -> Proof.state
val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
end;
@@ -378,16 +378,18 @@
fun merge data : T = Library.merge (eq_snd op =) data;
);
-fun gen_theorem schematic prep_att prep_stmt
- kind before_qed after_qed (name, raw_atts) raw_elems raw_concl int lthy =
+fun gen_theorem schematic prep_bundle prep_att prep_stmt
+ kind before_qed after_qed (name, raw_atts) raw_includes raw_elems raw_concl int lthy =
let
- val _ = Local_Theory.affirm lthy;
+ val _ = Local_Theory.assert lthy;
val thy = Proof_Context.theory_of lthy;
val attrib = prep_att thy;
+
val elems = raw_elems |> map (Element.map_ctxt_attrib attrib);
- val ((more_atts, prems, stmt, facts), goal_ctxt) =
- prep_statement attrib prep_stmt elems raw_concl lthy;
+ val ((more_atts, prems, stmt, facts), goal_ctxt) = lthy
+ |> Bundle.includes (map (prep_bundle lthy) raw_includes)
+ |> prep_statement attrib prep_stmt elems raw_concl;
val atts = more_atts @ map attrib raw_atts;
fun after_qed' results goal_ctxt' =
@@ -421,12 +423,13 @@
in
-val theorem' = gen_theorem false (K I) Expression.cert_statement;
-fun theorem a b c d e f = theorem' a b c d e f;
-val theorem_cmd = gen_theorem false Attrib.intern_src Expression.read_statement;
+val theorem = gen_theorem false (K I) (K I) Expression.cert_statement;
+val theorem_cmd =
+ gen_theorem false Bundle.check Attrib.intern_src Expression.read_statement;
-val schematic_theorem = gen_theorem true (K I) Expression.cert_statement;
-val schematic_theorem_cmd = gen_theorem true Attrib.intern_src Expression.read_statement;
+val schematic_theorem = gen_theorem true (K I) (K I) Expression.cert_statement;
+val schematic_theorem_cmd =
+ gen_theorem true Bundle.check Attrib.intern_src Expression.read_statement;
fun add_theorem_hook f = Theorem_Hook.map (cons (f, stamp ()));
--- a/src/Pure/Isar/toplevel.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Isar/toplevel.ML Wed Mar 21 23:41:22 2012 +0100
@@ -58,6 +58,8 @@
val theory': (bool -> theory -> theory) -> transition -> transition
val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition
val end_local_theory: transition -> transition
+ val open_target: (generic_theory -> local_theory) -> transition -> transition
+ val close_target: transition -> transition
val local_theory': (xstring * Position.T) option -> (bool -> local_theory -> local_theory) ->
transition -> transition
val local_theory: (xstring * Position.T) option -> (local_theory -> local_theory) ->
@@ -105,7 +107,7 @@
(* local theory wrappers *)
val loc_init = Named_Target.context_cmd;
-val loc_exit = Local_Theory.exit_global;
+val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
fun loc_begin loc (Context.Theory thy) = loc_init (the_default ("-", Position.none) loc) thy
| loc_begin NONE (Context.Proof lthy) = lthy
@@ -456,6 +458,20 @@
(fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (loc_exit lthy), SOME lthy)
| _ => raise UNDEF));
+fun open_target f = transaction (fn _ =>
+ (fn Theory (gthy, _) =>
+ let val lthy = f gthy
+ in Theory (Context.Proof lthy, SOME lthy) end
+ | _ => raise UNDEF));
+
+val close_target = transaction (fn _ =>
+ (fn Theory (Context.Proof lthy, _) =>
+ (case try Local_Theory.close_target lthy of
+ SOME lthy' => Theory (Context.Proof lthy', SOME lthy)
+ | NONE => raise UNDEF)
+ | _ => raise UNDEF));
+
+
local
fun local_theory_presentation loc f = present_transaction (fn int =>
--- a/src/Pure/Syntax/parser.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/Syntax/parser.ML Wed Mar 21 23:41:22 2012 +0100
@@ -201,7 +201,7 @@
val tk_prods =
these
(AList.lookup (op =) nt_prods
- (SOME (hd l_starts handle Empty => unknown_start)));
+ (SOME (hd l_starts handle List.Empty => unknown_start)));
(*add_lambda is true if an existing production of the nt
produces lambda due to the new lambda NT l*)
--- a/src/Pure/library.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Pure/library.ML Wed Mar 21 23:41:22 2012 +0100
@@ -328,7 +328,7 @@
fun single x = [x];
fun the_single [x] = x
- | the_single _ = raise Empty;
+ | the_single _ = raise List.Empty;
fun singleton f x = the_single (f [x]);
@@ -372,12 +372,12 @@
(* (op @) [x1, ..., xn] ===> ((x1 @ x2) @ x3) ... @ xn
for operators that associate to the left (TAIL RECURSIVE)*)
-fun foldl1 f [] = raise Empty
+fun foldl1 f [] = raise List.Empty
| foldl1 f (x :: xs) = foldl f (x, xs);
(* (op @) [x1, ..., xn] ===> x1 @ (x2 ... @ (x[n-1] @ xn))
for n > 0, operators that associate to the right (not tail recursive)*)
-fun foldr1 f [] = raise Empty
+fun foldr1 f [] = raise List.Empty
| foldr1 f l =
let fun itr [x] = x
| itr (x::l) = f(x, itr l)
@@ -454,7 +454,7 @@
in mapp 0 end;
(*rear decomposition*)
-fun split_last [] = raise Empty
+fun split_last [] = raise List.Empty
| split_last [x] = ([], x)
| split_last (x :: xs) = apfst (cons x) (split_last xs);
--- a/src/Tools/induct.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Tools/induct.ML Wed Mar 21 23:41:22 2012 +0100
@@ -104,12 +104,12 @@
val mk_var = Net.encode_type o #2 o Term.dest_Var;
-fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty =>
+fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle List.Empty =>
raise THM ("No variables in conclusion of rule", 0, [thm]);
in
-fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty =>
+fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle List.Empty =>
raise THM ("No variables in major premise of rule", 0, [thm]);
val left_var_concl = concl_var hd;
--- a/src/Tools/jEdit/etc/settings Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Tools/jEdit/etc/settings Wed Mar 21 23:41:22 2012 +0100
@@ -6,7 +6,7 @@
JEDIT_OPTIONS="-reuseview -noserver -nobackground -log=9"
JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss4m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
#JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
-JEDIT_SYSTEM_OPTIONS="-Dapple.laf.useScreenMenuBar=true -Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit"
+JEDIT_SYSTEM_OPTIONS="-Dapple.laf.useScreenMenuBar=false -Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit"
JEDIT_STYLE_SHEETS="$ISABELLE_HOME/etc/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css"
--- a/src/Tools/subtyping.ML Wed Mar 21 16:53:24 2012 +0100
+++ b/src/Tools/subtyping.ML Wed Mar 21 23:41:22 2012 +0100
@@ -832,7 +832,7 @@
"\nwhere C is a constructor and fi is of type (xi => yi) or (yi => xi).";
val ((fis, T1), T2) = apfst split_last (strip_type (fastype_of t))
- handle Empty => error ("Not a proper map function:" ^ err_str t);
+ handle List.Empty => error ("Not a proper map function:" ^ err_str t);
fun gen_arg_var ([], []) = []
| gen_arg_var ((T, T') :: Ts, (U, U') :: Us) =