src/FOL/blastdata.ML
changeset 11748 06eb315831ff
parent 10906 de95ba2760fe
child 16774 515b6020cf5d
equal deleted inserted replaced
11747:17a6dcd6f3cf 11748:06eb315831ff
     8   val contr_tac = Cla.contr_tac
     8   val contr_tac = Cla.contr_tac
     9   val dup_intr	= Cla.dup_intr
     9   val dup_intr	= Cla.dup_intr
    10   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    10   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
    11   val claset	= Cla.claset
    11   val claset	= Cla.claset
    12   val rep_cs    = Cla.rep_cs
    12   val rep_cs    = Cla.rep_cs
    13   val atomize	= atomize_rules
       
    14   val cla_modifiers = Cla.cla_modifiers;
    13   val cla_modifiers = Cla.cla_modifiers;
    15   val cla_meth' = Cla.cla_meth'
    14   val cla_meth' = Cla.cla_meth'
    16   end;
    15   end;
    17 
    16 
    18 structure Blast = BlastFun(Blast_Data);
    17 structure Blast = BlastFun(Blast_Data);