src/HOL/cladata.ML
changeset 7153 820c8c8573d9
parent 7007 b46ccfee8e59
child 7357 d0e16da40ea2
     1.1 --- a/src/HOL/cladata.ML	Mon Aug 02 17:58:23 1999 +0200
     1.2 +++ b/src/HOL/cladata.ML	Mon Aug 02 17:58:46 1999 +0200
     1.3 @@ -76,7 +76,8 @@
     1.4    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
     1.5    val claset	= Classical.claset
     1.6    val rep_cs    = Classical.rep_cs
     1.7 -  val cla_method' = Classical.cla_method'
     1.8 +  val cla_modifiers = Classical.cla_modifiers;
     1.9 +  val cla_meth' = Classical.cla_meth'
    1.10    end;
    1.11  
    1.12  structure Blast = BlastFun(Blast_Data);