--- a/src/Pure/Isar/rule_cases.ML Tue Sep 03 18:21:43 2013 +0200
+++ b/src/Pure/Isar/rule_cases.ML Tue Sep 03 19:58:00 2013 +0200
@@ -21,7 +21,7 @@
include BASIC_RULE_CASES
datatype T = Case of
{fixes: (binding * typ) list,
- assumes: (string * term list) list,
+ assumes: (binding * term list) list,
binds: (indexname * term option) list,
cases: (string * T) list}
val case_hypsN: string
@@ -62,7 +62,7 @@
datatype T = Case of
{fixes: (binding * typ) list,
- assumes: (string * term list) list,
+ assumes: (binding * term list) list,
binds: (indexname * term option) list,
cases: (string * T) list};
@@ -91,21 +91,22 @@
| extract_fixes (SOME outline) prop =
chop (length (Logic.strip_params outline)) (strip_params prop);
-fun extract_assumes _ _ NONE prop = ([("", Logic.strip_assums_hyp prop)], [])
- | extract_assumes qual hnames (SOME outline) prop =
+fun extract_assumes _ _ NONE prop = ([(Binding.empty, Logic.strip_assums_hyp prop)], [])
+ | extract_assumes qualifier hyp_names (SOME outline) prop =
let
+ val qual = Binding.qualify true qualifier o Binding.name;
val (hyps, prems) =
chop (length (Logic.strip_assums_hyp outline)) (Logic.strip_assums_hyp prop)
- fun extract ((hname,h)::ps) = (qual hname, h :: map snd ps);
- val (hyps1,hyps2) = chop (length hnames) hyps;
- val pairs1 = if hyps1 = [] then [] else hnames ~~ hyps1;
- val pairs = pairs1 @ (map (pair case_hypsN) hyps2);
- val named_hyps = map extract (partition_eq (eq_fst op =) pairs)
+ fun extract ((hyp_name, hyp) :: rest) = (qual hyp_name, hyp :: map snd rest);
+ val (hyps1, hyps2) = chop (length hyp_names) hyps;
+ val pairs1 = if null hyps1 then [] else hyp_names ~~ hyps1;
+ val pairs = pairs1 @ map (pair case_hypsN) hyps2;
+ val named_hyps = map extract (partition_eq (eq_fst op =) pairs);
in (named_hyps, [(qual case_premsN, prems)]) end;
fun bindings args = map (apfst Binding.name) args;
-fun extract_case thy (case_outline, raw_prop) name hnames concls =
+fun extract_case thy (case_outline, raw_prop) name hyp_names concls =
let
val props = Logic.dest_conjunctions (Drule.norm_hhf thy raw_prop);
val len = length props;
@@ -120,7 +121,8 @@
else
fold_rev Term.abs fixes1
(app (map (Term.dummy_pattern o #2) fixes2) (fold_rev Term.abs fixes2 t));
- val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) hnames case_outline prop
+ val (assumes1, assumes2) =
+ extract_assumes name hyp_names case_outline prop
|> pairself (map (apsnd (maps Logic.dest_conjunctions)));
val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
@@ -153,11 +155,11 @@
let
val n = length cases;
val nprems = Logic.count_prems prop;
- fun add_case ((name, hnames), concls) (cs, i) =
+ fun add_case ((name, hyp_names), concls) (cs, i) =
((case try (fn () =>
(Option.map (curry Logic.nth_prem i) rule_struct, Logic.nth_prem (i, prop))) () of
NONE => (name, NONE)
- | SOME p => (name, extract_case thy p name hnames concls)) :: cs, i - 1);
+ | SOME p => (name, extract_case thy p name hyp_names concls)) :: cs, i - 1);
in fold_rev add_case (drop (Int.max (n - nprems, 0)) cases) ([], n) |> #1 end;
in