57 val get_eqvts_thms = eqvts o  Context.Proof;

    57 val get_eqvts_thms = eqvts o  Context.Proof;

    58 val get_eqvts_raw_thms = eqvts_raw o Context.Proof;

    58 val get_eqvts_raw_thms = eqvts_raw o Context.Proof;

    59 

    59 

    60 val add_thm = EqvtData.map o Item_Net.update;

    60 val add_thm = EqvtData.map o Item_Net.update;

    61 val del_thm = EqvtData.map o Item_Net.remove;

    61 val del_thm = EqvtData.map o Item_Net.remove;

    65 

    62 

    66 fun add_raw_thm thm = 

    63 fun add_raw_thm thm = 

    67   case prop_of thm of

    64   case prop_of thm of

    68     Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update thm)

    65     Const ("==", _) $ _ $ _ => EqvtRawData.map (Item_Net.update thm)

    69   | _ => raise THM ("Theorem must be a meta-equality", 0, [thm]) 

    66   | _ => raise THM ("Theorem must be a meta-equality", 0, [thm])