src/HOL/Tools/res_hol_clause.ML
changeset 20864 bb75b876b260
parent 20791 497e1c9d4a9f
child 20865 2cfa020109c1
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Thu Oct 05 10:42:39 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Thu Oct 05 10:46:26 2006 +0200
     1.3 @@ -627,7 +627,7 @@
     1.4  (* convert literals of clauses into strings *)
     1.5  fun string_of_combterm1_aux _ (CombConst(c,tp,_)) = 
     1.6      let val tp' = string_of_ctyp tp
     1.7 -	val c' = if c = "equal" then "fequal" else c
     1.8 +	val c' = if c = "equal" then "c_fequal" else c
     1.9      in
    1.10  	(wrap_type (c',tp'),tp')
    1.11      end
    1.12 @@ -676,7 +676,7 @@
    1.13  
    1.14  fun string_of_combterm2 _ (CombConst(c,tp,tvars)) = 
    1.15      let val tvars' = map string_of_ctyp tvars
    1.16 -	val c' = if c = "equal" then "fequal" else c
    1.17 +	val c' = if c = "equal" then "c_fequal" else c
    1.18      in
    1.19  	c' ^ (ResClause.paren_pack tvars')
    1.20      end
    1.21 @@ -813,8 +813,8 @@
    1.22  	val funcs2 = case tp of T_FULL => Symtab.update ("typeinfo",2) funcs1
    1.23  				      | _ => funcs1
    1.24      in
    1.25 -	case tp of T_CONST => Symtab.update ("fequal",1) (Symtab.update ("hEXTENT",2) funcs2)
    1.26 -			 | _ => Symtab.update ("fequal",0) (Symtab.update ("hEXTENT",0) funcs2)
    1.27 +	case tp of T_CONST => Symtab.update ("c_fequal",1) funcs2
    1.28 +			 | _ => Symtab.update ("c_fequal",0) funcs2
    1.29      end;
    1.30  
    1.31  
    1.32 @@ -903,15 +903,14 @@
    1.33  	val conjectures = make_conjecture_clauses thms
    1.34          val (clnames,axclauses') = ListPair.unzip (make_axiom_clauses axclauses user_lemmas)
    1.35  	val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
    1.36 -	val clss = conjectures @ axclauses'
    1.37 -	val funcs = funcs_of_clauses clss arity_clauses
    1.38 -	and preds = preds_of classrel_clauses arity_clauses
    1.39  	and probname = Path.pack (Path.base (Path.unpack filename))
    1.40  	val (axstrs,_) =  ListPair.unzip (map clause2dfg axclauses')
    1.41  	val tfree_clss = map ResClause.dfg_tfree_clause (ResClause.union_all tfree_litss)
    1.42  	val out = TextIO.openOut filename
    1.43  	val helper_clauses = (#2 o ListPair.unzip o get_helper_clauses) ()
    1.44  	val helper_clauses_strs = (#1 o ListPair.unzip o (map clause2dfg)) helper_clauses
    1.45 +	val funcs = funcs_of_clauses (helper_clauses @ conjectures @ axclauses') arity_clauses
    1.46 +	and preds = preds_of classrel_clauses arity_clauses
    1.47      in
    1.48  	TextIO.output (out, ResClause.string_of_start probname); 
    1.49  	TextIO.output (out, ResClause.string_of_descrip probname);