--- a/src/HOL/Tools/Function/fun_cases.ML Sat Mar 08 13:49:01 2014 +0100
+++ b/src/HOL/Tools/Function/fun_cases.ML Sat Mar 08 21:08:10 2014 +0100
@@ -43,17 +43,16 @@
fun gen_fun_cases prep_att prep_prop args lthy =
let
- val thy = Proof_Context.theory_of lthy;
val thmss =
map snd args
|> burrow (grouped 10 Par_List.map (mk_fun_cases lthy o prep_prop lthy));
val facts =
- map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att thy) atts), [(thms, [])]))
+ map2 (fn ((a, atts), _) => fn thms => ((a, map (prep_att lthy) atts), [(thms, [])]))
args thmss;
in lthy |> Local_Theory.notes facts end;
val fun_cases = gen_fun_cases (K I) Syntax.check_prop;
-val fun_cases_cmd = gen_fun_cases Attrib.intern_src Syntax.read_prop;
+val fun_cases_cmd = gen_fun_cases Attrib.check_src Syntax.read_prop;
val _ =
Outer_Syntax.local_theory @{command_spec "fun_cases"}