--- a/src/Pure/Isar/expression.ML Thu Feb 20 21:55:37 2014 +0100
+++ b/src/Pure/Isar/expression.ML Thu Feb 20 23:16:33 2014 +0100
@@ -19,10 +19,12 @@
Proof.context -> (term * term list) list list * Proof.context
(* Declaring locales *)
- val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list ->
+ val cert_declaration: expression_i -> (Proof.context -> Proof.context) ->
+ Element.context_i list ->
Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
* Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
- val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list ->
+ val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) ->
+ Element.context list ->
Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
* Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
(*FIXME*)
@@ -39,13 +41,16 @@
(term list list * (string * morphism) list * morphism) * Proof.context
val read_goal_expression: expression -> Proof.context ->
(term list list * (string * morphism) list * morphism) * Proof.context
- val permanent_interpretation: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
- val ephemeral_interpretation: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
+ val permanent_interpretation: expression_i -> (Attrib.binding * term) list ->
+ local_theory -> Proof.state
+ val ephemeral_interpretation: expression_i -> (Attrib.binding * term) list ->
+ local_theory -> Proof.state
val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
val interpret_cmd: expression -> (Attrib.binding * string) list ->
bool -> Proof.state -> Proof.state
val interpretation: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
- val interpretation_cmd: expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
+ val interpretation_cmd: expression -> (Attrib.binding * string) list ->
+ local_theory -> Proof.state
val sublocale: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
val sublocale_cmd: expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
val sublocale_global: (local_theory -> local_theory) -> string -> expression_i ->
@@ -138,8 +143,11 @@
val implicit'' =
if strict then []
else
- let val _ = reject_dups
- "Parameter(s) declared simultaneously in expression and for clause: " (implicit' @ fixed')
+ let
+ val _ =
+ reject_dups
+ "Parameter(s) declared simultaneously in expression and for clause: "
+ (implicit' @ fixed');
in map (fn (x, mx) => (Binding.name x, NONE, mx)) implicit end;
in (expr', implicit'' @ fixed) end;
@@ -492,7 +500,8 @@
let
val (asm, defs) = Locale.specification_of thy name;
in
- (case asm of NONE => defs | SOME asm => asm :: defs) |> map (Morphism.term morph)
+ (case asm of NONE => defs | SOME asm => asm :: defs)
+ |> map (Morphism.term morph)
end;
fun prep_goal_expression prep expression context =
@@ -581,12 +590,13 @@
val (asm, defs) = Locale.specification_of thy loc;
val asm' = Option.map (Morphism.term morph) asm;
val defs' = map (Morphism.term morph) defs;
- val text' = text |>
- (if is_some asm
- then eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])])
+ val text' =
+ text |>
+ (if is_some asm then
+ eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])])
else I) |>
- (if not (null defs)
- then eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs'))
+ (if not (null defs) then
+ eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs'))
else I)
(* FIXME clone from locale.ML *)
in text' end;
@@ -618,7 +628,8 @@
val body = Object_Logic.atomize_term thy t;
val bodyT = Term.fastype_of body;
in
- if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
+ if bodyT = propT
+ then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
else (body, bodyT, Object_Logic.atomize (Proof_Context.init_global thy) (Thm.cterm_of thy t))
end;
@@ -700,7 +711,8 @@
if null exts then (NONE, NONE, [], thy)
else
let
- val abinding = if null ints then binding else Binding.suffix_name ("_" ^ axiomsN) binding;
+ val abinding =
+ if null ints then binding else Binding.suffix_name ("_" ^ axiomsN) binding;
val ((statement, intro, axioms), thy') =
thy
|> def_pred abinding parms defs' exts exts';
@@ -761,7 +773,9 @@
val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
val extraTs =
- subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
+ subtract (op =)
+ (fold Term.add_tfreesT (map snd parms) [])
+ (fold Term.add_tfrees exts' []);
val _ =
if null extraTs then ()
else warning ("Additional type variable(s) in locale specification " ^
@@ -790,14 +804,15 @@
[(Attrib.internal o K) Locale.witness_add])])])]
else [];
- val notes' = body_elems |>
- map (defines_to_notes pred_ctxt) |>
- map (Element.transform_ctxt a_satisfy) |>
- (fn elems =>
- fold_map assumes_to_notes elems (map (Element.conclude_witness pred_ctxt) a_axioms)) |>
- fst |>
- map (Element.transform_ctxt b_satisfy) |>
- map_filter (fn Notes notes => SOME notes | _ => NONE);
+ val notes' =
+ body_elems
+ |> map (defines_to_notes pred_ctxt)
+ |> map (Element.transform_ctxt a_satisfy)
+ |> (fn elems =>
+ fold_map assumes_to_notes elems (map (Element.conclude_witness pred_ctxt) a_axioms))
+ |> fst
+ |> map (Element.transform_ctxt b_satisfy)
+ |> map_filter (fn Notes notes => SOME notes | _ => NONE);
val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps;
val axioms = map (Element.conclude_witness pred_ctxt) b_axioms;
@@ -836,7 +851,8 @@
let
val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
val eqns = prep_with_extended_syntax prep_prop deps expr_ctxt raw_eqns;
- val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of initial_ctxt))) o fst) raw_eqns;
+ val attrss =
+ map (apsnd (map (prep_attr (Proof_Context.theory_of initial_ctxt))) o fst) raw_eqns;
val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
val export' = Variable.export_morphism goal_ctxt expr_ctxt;
in (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) end;
@@ -918,8 +934,10 @@
fun subscribe_locale_only lthy =
let
- val _ = if Named_Target.is_theory lthy
- then error "Not possible on level of global theory" else ();
+ val _ =
+ if Named_Target.is_theory lthy
+ then error "Not possible on level of global theory"
+ else ();
in subscribe lthy end;
@@ -929,7 +947,7 @@
before_exit raw_locale expression raw_eqns thy =
thy
|> Named_Target.init before_exit (prep_loc thy raw_locale)
- |> gen_local_theory_interpretation prep_interpretation subscribe_locale_only expression raw_eqns
+ |> gen_local_theory_interpretation prep_interpretation subscribe_locale_only expression raw_eqns;
in
--- a/src/Pure/Isar/rule_cases.ML Thu Feb 20 21:55:37 2014 +0100
+++ b/src/Pure/Isar/rule_cases.ML Thu Feb 20 23:16:33 2014 +0100
@@ -233,7 +233,8 @@
(case AList.lookup (op =) (Thm.get_tags th) consumes_tagN of
NONE => NONE
| SOME s =>
- (case Lexicon.read_nat s of SOME n => SOME n
+ (case Lexicon.read_nat s of
+ SOME n => SOME n
| _ => raise THM ("Malformed 'consumes' tag of theorem", 0, [th])));
fun get_consumes th = the_default 0 (lookup_consumes th);
@@ -262,7 +263,8 @@
(case AList.lookup (op =) (Thm.get_tags th) constraints_tagN of
NONE => NONE
| SOME s =>
- (case Lexicon.read_nat s of SOME n => SOME n
+ (case Lexicon.read_nat s of
+ SOME n => SOME n
| _ => raise THM ("Malformed 'constraints' tag of theorem", 0, [th])));
fun get_constraints th = the_default 0 (lookup_constraints th);
@@ -341,7 +343,8 @@
fun save_case_concls th =
let val concls = Thm.get_tags th |> map_filter
(fn (a, b) =>
- if a = case_concl_tagN then (case explode_args b of c :: cs => SOME (c, cs) | _ => NONE)
+ if a = case_concl_tagN
+ then (case explode_args b of c :: cs => SOME (c, cs) | _ => NONE)
else NONE)
in fold add_case_concl concls end;
@@ -385,7 +388,8 @@
(case lookup_case_names th of
NONE => map (rpair [] o Library.string_of_int) (1 upto (Thm.nprems_of th - n))
| SOME names => map (fn name => (name, get_case_concls th name)) names);
- val cases_hyps = (case lookup_cases_hyp_names th of
+ val cases_hyps =
+ (case lookup_cases_hyp_names th of
NONE => replicate (length cases) []
| SOME names => names);
fun regroup ((name,concls),hyps) = ((name,hyps),concls)
--- a/src/Pure/Isar/specification.ML Thu Feb 20 21:55:37 2014 +0100
+++ b/src/Pure/Isar/specification.ML Thu Feb 20 23:16:33 2014 +0100
@@ -46,7 +46,8 @@
val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option * string ->
bool -> local_theory -> local_theory
val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
- val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
+ val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list ->
+ local_theory -> local_theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
val theorems: string ->
@@ -90,7 +91,8 @@
(case duplicates (op =) commons of [] => ()
| dups => error ("Duplicate local variables " ^ commas_quote dups));
val frees = rev (fold (Variable.add_free_names ctxt) As (rev commons));
- val types = map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length frees));
+ val types =
+ map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length frees));
val uniform_typing = the o AList.lookup (op =) (frees ~~ types);
fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)