# HG changeset patch
# User bulwahn
# Date 1285246216 -7200
# Node ID b1febbbda458670c9e78613d28d4d8d75913af85
# Parent  2e06dad03dd32ecaa38210ebcd3071e759df955e
improving naming of assumptions in code_pred

diff -r 2e06dad03dd3 -r b1febbbda458 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Sep 23 14:50:15 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Sep 23 14:50:16 2010 +0200
@@ -3070,9 +3070,9 @@
     val cases_rules = map mk_cases preds
     val cases =
       map2 (fn pred_name => fn case_rule => Rule_Cases.Case {fixes = [],
-        assumes = ("", Logic.strip_imp_prems case_rule)
+        assumes = ("that", tl (Logic.strip_imp_prems case_rule))
           :: (map_filter (fn (fact_name, fact) => Option.map (rpair [fact]) fact_name)
-            ((SOME "prems" :: names_of ctxt' pred_name) ~~ Logic.strip_imp_prems case_rule)),
+            ((SOME (Long_Name.base_name pred_name ^ ".prems") :: names_of ctxt' pred_name) ~~ Logic.strip_imp_prems case_rule)),
         binds = [], cases = []}) preds cases_rules
     val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
     val lthy'' = lthy'