--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Tue Feb 10 14:48:26 2015 +0100
@@ -93,7 +93,8 @@
(def, lthy')
end;
- fun tac ctxt thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac ctxt thms);
+ fun tac ctxt thms =
+ Class.intro_classes_tac ctxt [] THEN ALLGOALS (Proof_Context.fact_tac ctxt thms);
val qualify =
Binding.qualify true (Long_Name.base_name fcT_name) o Binding.qualify true eqN o Binding.name;