Lines Matching defs:id
47 type clauseInfo = {parameters : parameters, id : clauseId, thm : Thm.thm};
60 fun pp (Clause {id,thm,...}) =
61 if !showId then ppIdThm (id,thm) else Thm.pp thm;
79 fun id (Clause {id = i, ...}) = i;
86 Clause {parameters = parameters, id = newId (), thm = thm};
207 (* Simplifying rules: these preserve the clause id. *)
210 fun freshVars (Clause {parameters,id,thm}) =
211 Clause {parameters = parameters, id = id, thm = Rule.freshVars thm};
213 fun simplify (Clause {parameters,id,thm}) =
216 | SOME thm => SOME (Clause {parameters = parameters, id = id, thm = thm});
218 fun reduce units (Clause {parameters,id,thm}) =
219 Clause {parameters = parameters, id = id, thm = Units.reduce units thm};
221 fun rewrite rewr (cl as Clause {parameters,id,thm}) =
228 Rewrite.rewriteIdRule rewr cmp id th
233 val () = Print.trace Print.ppInt "Clause.rewrite: id" id
238 case Rewrite.peek rewr id of
242 val result = Clause {parameters = parameters, id = id, thm = thm}
310 val cl = Clause {parameters = parameters, id = newId (), thm = th}
358 Clause {parameters = parameters, id = newId (), thm = th}