src/Pure/Isar/proof.ML
changeset 62663 bea354f6ff21
parent 61841 4d3527b94f2a
child 62771 dd2914250ca7
equal deleted inserted replaced
62662:291cc01f56f5 62663:bea354f6ff21
   171     before_qed: Method.text option,
   171     before_qed: Method.text option,
   172     after_qed:
   172     after_qed:
   173       (context * thm list list -> state -> state) *
   173       (context * thm list list -> state -> state) *
   174       (context * thm list list -> context -> context)};
   174       (context * thm list list -> context -> context)};
   175 
   175 
       
   176 val _ =
       
   177   PolyML.addPrettyPrinter (fn _ => fn _ => fn _: state =>
       
   178     Pretty.to_polyml (Pretty.str "<Proof.state>"));
       
   179 
   176 fun make_goal (statement, using, goal, before_qed, after_qed) =
   180 fun make_goal (statement, using, goal, before_qed, after_qed) =
   177   Goal {statement = statement, using = using, goal = goal,
   181   Goal {statement = statement, using = using, goal = goal,
   178     before_qed = before_qed, after_qed = after_qed};
   182     before_qed = before_qed, after_qed = after_qed};
   179 
   183 
   180 fun make_node (context, facts, mode, goal) =
   184 fun make_node (context, facts, mode, goal) =