src/Provers/blast.ML
changeset 32174 9036cc8ae775
parent 32091 30e2ffbba718
child 32176 893614e2c35c
equal deleted inserted replaced
32173:34f7b0fbe047 32174:9036cc8ae775
   179 fun mkGoal P = Const ("*Goal*", []) $ P;
   179 fun mkGoal P = Const ("*Goal*", []) $ P;
   180 
   180 
   181 fun isGoal (Const ("*Goal*", _) $ _) = true
   181 fun isGoal (Const ("*Goal*", _) $ _) = true
   182   | isGoal _ = false;
   182   | isGoal _ = false;
   183 
   183 
   184 val TruepropC = ObjectLogic.judgment_name (the_context ());
   184 val TruepropC = ObjectLogic.judgment_name (OldGoals.the_context ());
   185 val TruepropT = Sign.the_const_type (the_context ()) TruepropC;
   185 val TruepropT = Sign.the_const_type (OldGoals.the_context ()) TruepropC;
   186 
   186 
   187 fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t);
   187 fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t);
   188 
   188 
   189 fun strip_Trueprop (tm as Const (c, _) $ t) = if c = TruepropC then t else tm
   189 fun strip_Trueprop (tm as Const (c, _) $ t) = if c = TruepropC then t else tm
   190   | strip_Trueprop tm = tm;
   190   | strip_Trueprop tm = tm;