--- a/src/Pure/Isar/specification.ML Tue Jul 05 09:50:20 2016 +0200
+++ b/src/Pure/Isar/specification.ML Tue Jul 05 10:32:25 2016 +0200
@@ -93,6 +93,19 @@
(* prepare specification *)
+fun get_positions ctxt x =
+ let
+ fun get Cs (Const ("_type_constraint_", C) $ t) = get (C :: Cs) t
+ | get Cs (Free (y, T)) =
+ if x = y then
+ map_filter Term_Position.decode_positionT
+ (T :: map (Type.constraint_type ctxt) Cs)
+ else []
+ | get _ (t $ u) = get [] t @ get [] u
+ | get _ (Abs (_, _, t)) = get [] t
+ | get _ _ = [];
+ in get [] end;
+
local
fun prep_decls prep_var raw_vars ctxt =
@@ -120,19 +133,6 @@
val (tss', _) = (fold_map o fold_map) Term.free_dummy_patterns tss names;
in tss' end;
-fun get_positions ctxt x =
- let
- fun get Cs (Const ("_type_constraint_", C) $ t) = get (C :: Cs) t
- | get _ (t $ u) = get [] t @ get [] u
- | get _ (Abs (_, _, t)) = get [] t
- | get Cs (Free (y, T)) =
- if x = y then
- map_filter Term_Position.decode_positionT
- (T :: map (Type.constraint_type ctxt) Cs)
- else []
- | get _ _ = [];
- in get [] end;
-
fun prep_spec_open prep_var parse_prop raw_vars raw_params raw_prems raw_concl ctxt =
let
val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt;
@@ -240,7 +240,7 @@
let
val atts = map (prep_att lthy) raw_atts;
- val ((vars, xs, get_pos, spec), spec_ctxt) = lthy
+ val ((vars, xs, get_pos, spec), _) = lthy
|> prep_spec (the_list raw_var) raw_params raw_prems raw_spec;
val (((x, T), rhs), prove) = Local_Defs.derived_def lthy {conditional = true} spec;
val _ = Name.reject_internal (x, []);
@@ -279,7 +279,7 @@
fun gen_abbrev prep_spec mode raw_var raw_params raw_spec int lthy =
let
val lthy1 = lthy |> Proof_Context.set_syntax_mode mode;
- val ((vars, xs, get_pos, spec), spec_ctxt) = lthy
+ val ((vars, xs, get_pos, spec), _) = lthy
|> Proof_Context.set_mode Proof_Context.mode_abbrev
|> prep_spec (the_list raw_var) raw_params [] raw_spec;
val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 spec));